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.