How is axiom of choice utilized within the given proof? I (only a beginner in set theory...) want to see a prove that an infinite set must have an infinite countable subset U:
The following answer sounds quite logically for me:
John Wayland Bales, Prove that every infinite set has a countable subset
However, I guess that this proof depends at least on on some weaker variant of axiom of choice.
John Wayland Bales constructs a series of non empty finite sets with increasing number of elements:

For each $N\in\mathbb{N}$, $S$ contains an element distinct from each
element in $U_N=\{x_1,x_2,\cdots,x_n\}$, so define
$U_{N+1}=U_N\cup\{x_{N+1}\}$ where $x_{N+1}$ is an element of $S$
distinct from each element of $U_N$.

Where is AC hidden in this argumentation?
I feel, that the last step is critical:

Let $$U=\bigcup_{N\in\mathbb{N}}U_N$$
Then $U$ is a countable subset of $S$.

I would like to learn, how the proof is done "correctly" by using AC or some weaker weaker variant (axiom of countable choice...).
My problem: Of course I see that recursive choices of "any" elements to create a new set are crucial, but those choices are done sequentially and not on an infinite set of sets that is already "available" and clearly defined. AC (in it's original textbook variant) is about the latter situation and not about a set, that is still in process of being constructed.
 A: This proof is a great example of how subtle the use of the Axiom of Choice can be.
You are kind of right that the last step is the critical step, but in fact, the whole thing is just a big appeal to the Axiom of Choice.
Definitions by recursion, in general, require you to specify a function which takes in as input your "intermediate step" and produces the next step. But here we don't have a function, we have a relation. We simply say "we can add one more element!", but the choice of this element can be very different and it will result in a different input during the next step of the recursion.
So the claim that the set $\{U_n\mid n\in\Bbb N\}$ even exists is appealing to the Principle of Dependent Choice, which is a sort of countable version of Zorn's lemma, if you will, or a slight strengthening of the Axiom of Countable Choice (although some people will mistakenly assume that that is what Countable Choice mean). We can use the Axiom of Choice, as a whole, by first fixing a choice function and then using it to choose the next element in each step.
Removing that assumption, the proof merely shows that for all $n\in\Bbb N$, an infinite set would have a subset of size $n$. In other words, an infinite cardinal is always larger than all finite cardinals.
Now, you're right of course, that the union of the finite sets need not be itself countable, but here we actually have a way around this: every $U_n$ has exactly $n$ elements, and $U_n\subseteq U_m$ for $n\leq m$. So that means $u_n$ is the unique element in $U_{n+1}\setminus U_n$, and that gives us an enumeration of the union, assuming of course that $\{U_n\mid n\in\Bbb N\}$ exists.
A: First of all, a set $S$ is infinite iff it can't be put in bijection with $\varnothing$ or $I_n=\{1,2,...,n\} \ \ \forall n \in \mathbb{N}$. This implies that if $S$ is infinite ,it is not empty.
Formally speaking the recursion(where $x_1$ is a fixed element of $S$ that exists since $S\neq \varnothing$):
$$
\left\{
\begin{array}{c}
U_{1}=\{x_1\} \\
U_{n+1}=U_n \cup \{x_{n+1}\} \ \ \ x_{n+1}\in S/U_{n}
\end{array}
\right.
$$
Is ill-posed because it doesn't specify what is $x_{n+1}$.For example if $S=\mathbb{R}$ and $U_1=\{\pi\}$, who is $U_2$? It is not univocally determined , it may be $\{\pi,e\}$, it may be $\{\pi,2\}$,...
So this recursion is ill posed. To make this recursion well-posed we need something that takes "in input" $S/U_{n}$ and gives us an element of $S/U_{n}$ univocally for all $n$. The idea is to construct a choice function:
$$\Gamma: \mathcal{P}(S)/\{\varnothing \} \to S
$$
So that we can define the recursion as:
$$
\left\{
\begin{array}{c}
U_{1}=\{x_1\} \\
U_{n+1}=U_n \cup \{\Gamma (S/U_n)\} 
\end{array}
\right.
$$
Notice that this recursion is well posed since $S/U_n$ is non-empty for all $n$, so it can be an argument of choice function. Indeed if it was $S/U_n=\varnothing$ then $S=U_n$, but $S$ is infinite so $S\neq U_n$ (contradiction!).
