Equivalence of Dedekind infinity and infinity, and Axiom of Choice Lemma
Let $X$ be an infinite set. Then:


*

*$X$ contains a countable subset $N$ such that $N^C=X\smallsetminus N$ is infinite;

*For any such $N\subseteq X$, $X$ is in bijection with $N^C$.


Proof.


*

*Pick $x_1\in X$. $X\smallsetminus\{x_1\}\neq\varnothing$, so there exists $x_1\neq x_2\in X$. Call $F_1:=\{x_1\},F_2:=\{x_2\}$. Now, $X\smallsetminus F_2\neq\varnothing$, as $X$ is infinite and $F_2$ is finite. So there exists $x_3\in X\smallsetminus F_2$. Call $F_3:=F_2\cup\{x_3\}$. Rinse and repeat, and with enough repetitions, for any $n$, there is $F_n$ with $n$ elements such that $F_1\subseteq F_2\subseteq\dotso\subseteq F_n\subseteq\dotso$. Now set $N:=\bigcup_nF_n$. Set $f_1:\{1\}\to F_1$ by $f_1(1)=x_1$. Set $f_2:\{1,2\}\to F_2$ by $f_2(1)=x_1,f_2(2)=x_2$. Now $f_1$ can be viewed as $f_2|_{\{1\}}$. Go on like this, and for any $n$ you have $f_n:\{1,\dotsc,n\}\to F_n$, and $f_n|_{\{1,\dotsc,n-1\}}=f_{n-1}$ (modulo viewing $f_{n-1}$ as a $F_n$-valued function). Set $f(i)=f_i(i)$. This is a function defined on $\mathbb N$ and taking values in $F$, and satisfies $f|_{\{1,\dotsc,i\}}=f_i$ (modulo viewing $f_i$ as $F$-valued). Clearly it is defined on all $\mathbb N$, since for any $i$ there is an $f_i$. Suppose $f(n_1)=f(n_2)$. Then, if $m:=\max\{n_1,n_2\}$, $f_m(n_1)=f_m(n_2)$, but all $f_i$ are injective, so $n_1=n_2$, making $f$ injective too. If $f$ is surjective, item 1 is proved. But any $x\in F$ must belong to an $F_i$, so there is $f_i$ which has it as a value, that is we have $k\leq i:f_i(k)=x$, but then $f(k)=x$, proving $f(\mathbb N)=F$. If $F^C$ is not infinite, just pick $N:=f(2\mathbb N)$ as your new countable set, and its complement will be $F^C\cup f(2\mathbb N+1)$, which is a superset of the countable $f(2\mathbb N+1)$ and therefore must be infinite.

*Let $N=\{x_1,\dotsc,x_n,\dotsc\}$. By 1, $N$ contains a countable subset $M=\{y_1,\dotsc,y_n,\dotsc\}$. Let us construct $f:N^C\to X$ which is bijective. If $x\in N^C\smallsetminus M$, set $f(x)=x$. If $x\in M$, it will be a $y_n$, so we can set $f(y_n)=y_{\frac n2}$ if $n$ is even, and $f(y_n)=x_{\frac{n+1}{2}}$ if $n$ is odd. $f$ is clearly injective, and it is also surjective. Indeed, let $x\in X$. If $x\in N^C\smallsetminus M$, then $f(x)=x$, so $x$ is its own preimage. If $x=y_k$, its preimage is $y_{2k}$. If $x=x_k$, then its preimage is $y_{2k-1}$.


Corollary
$X$ is infinite iff there exists $A\subsetneq X$ such that $A,X$ are in bijection.
Proof.


*

*If $X$ is finite, it is in bijection with $\{1,\dotsc,n\}$ for some
$n$. We now show those are not in bijection with any of their proper
subsets by induction on $n$. If $n=1$, the only proper subset is the
empty set, which is clearly not in bijection with $\{1\}$. Suppose we
have proved our claim for $n-1$. Assume by way of contradiction there
exists $f:\{1,\dotsc,n\}\to\{1,\dotsc,n\}\smallsetminus\{x\}$ for
some $x\leq n$, with $f$ bijective. Pick $y\leq n$ such that $y\neq
   x$. $f|_{\{1,\dotsc,n\}\smallsetminus\{y\}}$ will be a bijection from
its domain to $h:=\{1,\dotsc,n\}\smallsetminus\{x,y\}$. Then again,
if we set $g(k)=k$ for $k<y$ and $g(k)=k-1$ for $k>y$, $g$ is
bijective from $\{1,\dotsc,n\}\smallsetminus\{y\}$ to
$\{1,\dotsc,n-1\}$, and $\tilde
   g:=g|_{\{1,\dotsc,n\}\smallsetminus\{x,y\}}$ is bijective from its
domain to $\{1,\dotsc,n-1\}\smallsetminus\{g(x)\}$, so that $\tilde
   g^{-1}\circ h\circ g$ is a bijection from $\{1,\dotsc,n-1\}$ to
$\{1,\dotsc,n-1\}\smallsetminus\{g(x)\}\subsetneq\{1,\dotsc,n-1\}$,
which contradicts the induction hypothesis.

*As for an infinite set, we have an $N$ such as is given by the above
lemma, and the same lemma gives us $N^C\subsetneq X$ is in bijection
with $X$, thus completing the proof.


Seems like a pretty solid and choice-free proof, right? Except there must be a catch, either here, or in Wikipedia, which seems (1 and 2 and 3) to state that the above is not provable without some weaker form of countable choice. Yet I seem to only have used finite choice and set operations above. So what am I missing? What am I implicitly using above that is not available in plain [ZF}(https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_theory)?
 A: 
Rinse and repeat, and with enough repetitions...

This "repetition" is not valid in first-order logic.  For any particular finite $n$, you can repeat the argument $n$ times to prove the existence of elements $x_1,\dots,x_n$ with the properties you want.  But you can't repeat it infinitely many times; that would make your proof infinitely long.  (Not to mention that even if you could have a next step in the proof after these infinitely many steps, there is no axiom of ZFC that would allow you to cobble these infinitely many elements $x_n$ into a single set, since you have no single formula that can refer to all of them.)
To formalize an infinite iterative process like this in ZF(C), you must use recursion.  Specifically, you can prove a theorem that says if you have some function $G$ defined on finite tuples, then there exists a unique infinite sequence $(x_n)$ such that $x_n=G(x_1,\dots,x_{n-1})$ for each $n$.  But to use this theorem, you need to already have this function $G$, and it needs to be a function: it needs to uniquely tell you how to choose $x_n$ given $x_1,\dots,x_{n-1}$.  The procedure you describe is just, "pick $x_n$ to be some element of $X$ that is not equal to any of $x_1,\dots,x_{n-1}$", but this does not define a function since this $x_n$ is not uniquely determined.
Using the axiom of choice, you can fix this.  In particular, at the start of your proof you can invoke the axiom of choice to let $C$ be a choice function on all the nonempty subsets of $X$, and then you can define $G(x_1,\dots,x_{n-1})=C(X\setminus\{x_1,\dots,x_{n-1}\})$.
So, in brief, the axiom of choice is needed to simultaneously choose all of the infinitely many elements $x_n$ you will use in your construction.
