I'm trying to prove that any infinite set $X$ contains a countable (denumerable) set. Please note that I want to prove this using countable choice.
All I ccould show by induction is that for each $n\in\mathbb{N}$, there exists an injection from $\{0, \dots, n\}$ into $X$. My first attempt was to choose such an injection for each $n\in\mathbb{N}$ (by $\textsf{ACC}$), take the union of the ranges of these functions and then come up with a bijection between that union and $\mathbb{N}$. But that was overly complicated for me (not wanting to use the fact that countable union of countable sets is countable). Hence, I tried formalizing the following idea.
Since $X$ is nonempty, there exists an $x_0\in X$. Now, since $X\setminus\{x_0\}$ is infinite again and hence nonempty, there exists an $x_1\in X\setminus\{x_0\}$. I guess that this should continue forever and I should be able to form a sequence $(x_n)_{n=0}^\infty$ such that each of the $x_n$'s are disntinct and hence create a bijection with $\mathbb{N}$.
But I'm not able to formalize this above intuition. Any help appreciated.
Best Answer
The naive idea that you have now is using Dependent Choice. The choice of $x_1$ depends on the choice of $x_0$, and so on. You would have avoided choice if you had a unique choice to make for $x_1$, etc., but in that case you already have a countably infinite subset which is circular. The complicated approach is the correct one.
Choose a set of size $n+1$, for each $n$. Here we use choice from the family of sets $\{[X]^{n+1}\mid n\in\Bbb N\}$, where $[X]^k$ is $\{X_0\subseteq X\mid k=|X_0|\}$. None of the $[X]^{n+1}$ is empty, since $X$ is infinite.
For each of these sets choose an enumeration, that is a bijection between the set and $\{0,\dots,n\}$. Here we again use choice: if $X_n$ is the $n$th chosen set, then $S_n=\{f\colon\{0,\dots,n\}\to X_n\mid f\text{ is a bijection}\}$ is non-empty for all $n$.
Now recursively, pick the smallest in said enumeration which hasn't appeared in your collection yet, such smallest exists because at the $n$th step you've collected $n$ elements, but the set has $n+1$ elements.
This does not require any choice, since the enumerations are already given. So we can specify "smallest" and this is a unique element from each $X_n$.
This is just a cleaned up version of your idea. But the point is that this only uses Countable Choice, since we only used it to choose the sets and the enumerations (which we can choose in a single go, actually, by choosing an injection from $\{0,\dots,n\}$ into $X$ for each $n$).
Alternatively, you can choose $X_n$ to have size $(n+1)^{n+1}$, then $Y_n=X_n\setminus\bigcup_{k<n}X_k$ is always non-empty, and then we can apply choice to $\{Y_n\mid n\in\Bbb N\}$.
(Again, Countable Choice is needed to get these $X_n$'s as well as choosing from the $Y_n$'s.)