I appreciate that this question has been asked a lot, but I'm hoping that the way that this question is formulated will be distinct from the currently available options. Here's my question:
Carefully prove, using the axioms of ZF along with the existence of choice functions, that if $A$ is a countable set whose elements are themselves countable, then $\cup A$ is countable.
I think I have a proof, and would be grateful if someone could provide feedback.
The steps I plan on proving are the following:
1) There is a surjection from $\mathbb{N}\times\mathbb{N}$ to $\cup A$.
2) For non-empty sets X and Y, there is an injection from X to Y, if and only if there is a surjection from Y to X.
3) There is an injection from $\mathbb{N}\times\mathbb{N}$ to $\mathbb{N}$.
Then an application of the three of these will give the result.
1) Firstly, consider the collection $\mathscr{F}$ of all functions from $\mathbb{N}$ to $\mathscr{A} = \cup A$. This exists as a set since we may comprehend it out of the set of subsets of ordered pairs between $\mathbb{N}$ and $\mathscr{A}$ given by $\mathcal{P}(\mathcal{P}(\mathbb{N}\times\mathscr{A}))$.
Then for each $a \in A$ we may comprehend the subset $\mathscr{F}_{a} = \{ f \in \mathscr{F} \mid \operatorname{Range}(f) = a \}$. Then since every element of $A$ is countable, $\mathscr{F}_{a} \neq \varnothing$ for any $a \in A$.
Then we may define the function $F : A \rightarrow \mathcal{P}(\mathcal{P}(\mathbb{N}\times\mathscr{A}))$ such that $a \mapsto \mathscr{F}_{a}$.
Then, since we are assuming that sets have choice functions, in particular $\mathcal{P}(\mathbb{N}\times\mathscr{A})$ has a choice function. So there exists $F_{C} : \mathcal{P}(\mathcal{P}(\mathbb{N}\times\mathscr{A})) \backslash \{\varnothing\} \rightarrow \mathcal{P}(\mathbb{N}\times\mathscr{A}))$ such that $F_{C}(S) \in S$ for all $S \in \mathcal{P}(\mathcal{P}(\mathbb{N}\times\mathscr{A})) \backslash \{\varnothing\}$.
Then, since Range$(F) \subseteq \mathcal{P}(\mathcal{P}(\mathbb{N}\times\mathscr{A})) \backslash \{\varnothing\}$, we can define the composition $$G = (F_{C} \circ F) : A \rightarrow \mathcal{P}(\mathbb{N} \times \mathscr{A})$$
Then $G$ is a function that takes an element $a$ of $A$ and returns a function in $\mathscr{A}^{\mathbb{N}}$ whose range is precisely $a$.
Then our original set $A$ is countable so there exists a surjective map $\ f : \mathbb{N} \rightarrow A$. Then we define the map:
\begin{align*} && H:\mathbb{N}^{2} \rightarrow \mathscr{A}, && (n,m)\mapsto (G(n))(m) & \end{align*}
Then $H \in \mathscr{A}^{\mathbb{N}\times\mathbb{N}}$, and further suppose $\alpha \in \mathscr{A}$, then there exists $a\in A$ such that $\alpha \in a$. Then since $f$ is surjective there exists $n \in \mathbb{N}$ such that $f(n) = a$. Then $G(a)$ is a map from $\mathbb{N}$ whose range is precisely $a$, so in particular there exists a $m\in\mathbb{N}$ such that $(G(a))(m) = \alpha$. Hence by construction $H(n,m) = \alpha$, and so $H$ is surjective.
2a) Now let $X$ and $Y$ be non-empty sets and suppose first that $\ f: X \hookrightarrow Y$. Suppose that \begin{align*} & F: \mathcal{P}(X) \backslash \{ \varnothing \} \rightarrow X, && F(A) \in A && \end{align*} Is a choice function for $X$ and let $x = F(X)$ (I'm not sure if this step is strictly needed?).
Then let $Y_{1}=\operatorname{Range}(f)$. Then $f$, considered as an element of $(Y_{1})^{X}$, is a bijection so there is a well defined inverse $G:Y_{1} \rightarrow X$. Then let $H = (Y \backslash Y_{1}) \times \{x\}$, then $H$ is a function that maps every element of $(Y \backslash Y_{1})$ to $x$. Then $S = G\cup H$ is a well defined function with domain $Y$ (since $(Y \backslash Y_{1}) \cap Y_{1} = \varnothing$) and clearly $S$ is surjective.
2b) Now suppose $f: Y \twoheadrightarrow X $ is a surjection, and let $F$ be a choice function for $Y$. Then for $x \in X$ we may comprehend the sets $Y_{x} = \{ y \in Y \mid f(y) = x\}$. Then $f$ is surjective so $Y_{x} \neq \varnothing $ for any $x\in X$. So we may construct the function $G$ that takes elements of $x$ and returns the subsets $Y_{x}$. Then $G$ is a function from $X$ in to $\mathcal{P}(Y) \backslash \{\varnothing\}$, so we may construct the composition $H = F \circ G$. Then $H$ is a function from $X$ to $Y$. Further since $f$ is a function, and so $Y_{x} \cap Y_{x'} = \varnothing$ for any distinct $x,x' \in X$, we have that $G$ is injective, and further, again since $Y_{x} \cap Y_{x'} = \varnothing$, $F$ is injective on the range of $G$. Hence $H$ is injective.
3) This one is an easy application of the uniqueness of the prime factorisation of elements of $\mathbb{N}$. Define $f : \mathbb{N} \times \mathbb{N} \rightarrow \mathbb{N}$ such that $(n,m) \mapsto (2^{n+1})\cdot (3^{m+1})$. Then it is clear that $f$ is injective.
Then, by 2) and 3) there exists surjection $F : \mathbb{N} \rightarrow \mathbb{N} \times \mathbb{N}$. Then we compose $F$ with the function $H$ we constructed in part 1) to get a surjective function $G$ whose domain is $\mathbb{N}$ and image is $\mathscr{A} = \cup A$. Hence $\cup A$ is countable.
I'm sure that this isn't the most efficient way of solving this problem, but is this a valid way of doing it with the choice function version of the axiom of choice?
In the below, I use the standard abbreviation "AC" for the axiom of choice, i.e, the principle of the existence of choice functions, to use your terminology.
You don't need AC for part (2a): if $X$ and $Y$ are non-empty and $f : X \to Y$ is injective, let $x$ be any element of $X$ and define $g(y)$ to be $f^{-1}(y)$ if $y$ is in the range of $f$ and to be $x$ otherwise. Then $g : Y \to X$ is surjective.
You do need AC for part (2b). In fact, AC is equivalent to the fact that any surjection has a right inverse. However, you don't need part (2b): in (2) you just need to get a surjection of $\Bbb{N}$ onto $\Bbb{N\times N}$ from the injection of $\Bbb{N}\times\Bbb{N}$ into $\Bbb{N}$ given by part (3).
So your proof is good, but you only need to appeal to AC for part (1).