Proving Dedekind finite implies finite assuming countable choice I'd like to show that if a set $X$ is Dedekind finite then is is finite if we assume $(AC)_{\aleph_0}$. As set $X$ is called Dedekind finite if the following equivalent conditions are satisfied: (a) there is no injection $\omega \hookrightarrow X$ (b) every injection $X \to X$ is also a surjection.
Countable choice $(AC)_{\aleph_0}$ says that every contable family of non-empty, pairwise disjoint sets has a choice function. 
There is the following theorem: 

from which I can prove what I want as follows: Pick an $x_0 \in X$. Define $G(F(0), \dots, F(n-1)) = \{x_0\}$ if $x_0 \notin \bigcup F(k)$ and $G(F(0), \dots , F(n-1)) = X \setminus \bigcup F(k)$ otherwise. Also, $G(\varnothing) = \{x_0\}$. Let $F: \omega \to X$ be as in the theorem. Then $F$ is injective by construction. 
The problem with that is that I suspect that the proof of theorem 24 needs countable choice. So what I am after is the following: consider the generalisation of theorem 24: 

(note the typo in $(R^\ast)$, it should be $F(z) \in G^\ast (F \mid I(z), z)$), and its proof (assuming AC): 

I want to modify this proof to prove the countable version of the theorem. But I can't seem to manage. I need a countable set $\{G^\ast \mid \{\langle f,z \rangle \} : \langle f,z \rangle \in dom(G^\ast) \}$. Ideas I had were along the lines of picking $f_0(x) = x_0$ the constant function and then to consider $\{G^\ast \mid \{\langle f_0,n \rangle \} : \langle f_0,n \rangle \in dom(G^\ast) \}$ but what then?
Thanks for your help.
 A: Let $X$ be an infinite set. For $n\in\omega$ let $$A_n=\{\langle a_0,\ldots,a_{n-1}\rangle\mid\forall i: a_i\in X\land\forall i,j: i\neq j\implies a_i\neq a_j\}$$
Because $X$ is infinite every $A_n$ is non-empty.
Use countable choice to choose $f_n\in A_n$. Now show that the union of the ranges of the $f_n$ is an enumerated union which is therefore well-ordered. This union cannot be finite, otherwise there would be some $f_k$ in which appears an element not in the union. Therefore it is countably infinite, as wanted.

Note that generally the principle of recursive construction is in fact stronger than countable choice and it is equivalent to the principle of Dependent Choice. (In fact this appears in the paragraph after the exercise you are trying to solve.)
A: To answer your first question (Dedekind finite implies finite), not your second (principle of generalised recursive constructions): we prove the contrapositive, showing that infinite implies Dedekind-infinite.
Suppose $X$ is infinite, i.e. has no bijection with $\{1 \ldots n \}$, for any $n \in \omega$.  Then by induction on $n$, there exists for each $n \in \omega$ some injection $f : \{1 \ldots n\} \to X$.
By countable choice, choose for each $n$ some such injection $f_n$.  Now define an injection $f_\omega : \omega \to X$ by taking $f_\omega(n)$ to be $f_n(i)$, for the least $i$ such that $f_n(i)$ has not perviously appeared as a value of $f_\omega(n)$.
This gives an injection $\omega \to X$, showing that $X$ is Dedekind-infinite, as desired.
