Every infinite set contains a countable subset

Assuming the axiom of choice, it can be shown that every infinite set contains a countable subset. Also, it is my understanding that the proof of this statement requires at least countable choice - i.e., it is consistent with ZF that there exist infinite sets which contain no countable subset.

However, consider the following proof:

Given an infinite (i.e. not equinumerous to any natural number) set $S$, let $A_1$ be a set containing one element in $S$, and construct $A_n$ by adding to $A_{n-1}$ any element from $S$ not already in $A_{n-1}$. This can be done since $S$ is finite, so at no point is $A_{n-1}$ equal to all of $S$. We can construct every $A_n$ using only ZF, since we are only making finitely many choices. Now, define $f: \mathbb{N} \rightarrow S$ by defining $f(n)$ to be the unique element in $A_n \backslash A_{n-1}$. $f$ is injective since $f(n) \notin A_m$ for every $m < n$, so $f(n) \neq f(m)$. Hence, $f$ is an injection from $\mathbb{N}$ to $S$, and the image of $f$ is a countable subset of $S$.

My problem is figuring out where in this proof the axiom of choice is used. It seems the construction of the $A_n$'s can be done without AC, since we are only making a finite number of choices. The construction of $f$ involves choosing an element from $A_n \backslash A_{n-1}$, but since we have a systematic way for choosing (take the unique element in the set) that should be allowed. I know this proof must depend on the axiom of choice, but where is it used?

The issue is that induction only tells you that something is true for every finite integer.

For example, by induction we can prove that every natural number $n$ has exactly $n$ predecessors ($0$ is a natural number). Does that mean that there exists a natural number with infinitely many predecessors? No. It does not.

Similarly here. If $A$ is an infinite set, without the axiom of choice we can prove that for every $n$ there is a subset of $A$ of size $n$. But can we prove there exists a subset equipotent with $\Bbb N$ itself? No. That requires us more. That requires that the choices we made during the inductive proof were coherent with one another, which essentially tells us that there is some sort of choice function that we can work with.

And indeed, without the axiom of choice, it is consistent that there are infinite sets without countably infinite subsets. These are called Dedekind-finite sets.

Perhaps the following elaboration is going to clarify this issue. Let's look at what the inductive proof really does.

You start with the empty set, and you have $A$ to choose from. That gives you $|A|$ many choices for a first element in your sequence. Suppose that you managed to get through $n$ choices, that gives you $|A|-n$ many choices to continue, and that's fine, since $|A|$ is not a finite integer, we can always make at least one choice and continue the construction.

But what are we really constructing? It's a tree of options. We start with the root, which is the empty sequence. Then at each step, we have splitting according to our options. In this case, however, there are infinitely many splittings at each step.

The inductive construction simply tells us that we constructed a tree without maximal points. The axiom of choice tells us that this tree has a branch, which in turn can be translated into a countably infinite subset. But the existence of a branch relies heavily on the axiom of choice. Why would you choose the first element to be one and not another? How about the second element? There is no canonical preference to make here, in the arbitrary case.

So what happens is that without choice, you might end up with a tree that has no maximal nodes, but no infinite branches either.

(In Mitchell Spector's answer he discusses inductive definitions, in that case, there is a function which chooses "the next step", so the tree is in fact a unique branch, and everything is fine. But in the proof you suggest, there is no such function, you appeal to choosing arbitrary elements at each step.)

I think it will clarify things to think about how you would actually set up the definition of the $A_n$ by induction. Spelling it out in detail will show exactly where the axiom of choice is used.

First, the formal principle of definition by mathematical induction that you are using looks like this:

Principle of definition by mathematical induction:

To define a function $f$ from $\omega$ to a set $E$ by induction, start with a function $g\colon E \to E$ and a specific $e_0\in E.$ You can then conclude that there is a unique $f\colon\omega\to E$ such that for all $n\lt\omega,$ $$f(n)=\begin{cases}e_0,&\text{ if }n=0, \\ g(f(n-1)),&\text{ if }n\gt 0. \end{cases}$$

(There are variants—for example, $g$ can be allowed to depend on $n$ also, or you could set things up for strong induction, but the above is sufficient for what you're doing.)

The function $f$ you are defining by induction is $n\mapsto A_n.$ To fit it into the above template, you can set $E$ equal to the collection of all finite subsets of $S$ (where $S$ is the infinite set that you are starting out with), and you can set $e_0=\emptyset$ (you actually started out with $A_1$ being a $1\text{-element}$ set, but this is easier).

But what are you going to use for $g?$

For your construction to work, the function $g\colon E\to E$ needs to satisfy the following property:

For any finite subset $X$ of $S,$ $g(X)\in S\setminus X.$

It's true that for any finite subset $X$ of $S,$ the set $S\setminus X$ is non-empty. Nevertheless, it requires a use of the axiom of choice to conclude that there is a function $g$ with domain $E$ such that for all $X$ in $E,$ $\;g(X)\in S\setminus X.$