Countable unions and the axiom of countable choice Let us denote by ACC the axiom of countable choice, namely the assertion that the product of countably many non-empty sets is non-empty, and denote by UCC the assertion that a countable union of countable sets is countable.
UCC is a simple theorem of ZF+ACC.
Proof Suppose for every $i\in\omega$ we have $X_i$ a countable set, and $X_i\cap X_j=\varnothing$ for $j\neq i$. 
Since $X_i$ is countable $O_i=\{f\colon X_i\to\omega\mid f\ \text{ injective}\}$ is non-empty. We can choose $f_i\in O_i$ by the axiom of countable choice, and define: $$F\colon\bigcup X_i\to \omega\times\omega\colon\qquad x\mapsto\langle n,f_n(x)\rangle$$
Where $n$ is the unique $n\in\omega$ such that $x\in X_n$.
The Cantor pairing function shows that $\omega\times\omega$ is countable and we are done.

Is the opposite assertion is true, namely ZF+UCC implies ACC? If the answer is negative, does that imply at least some other weaker form of choice?


*

*As noted by Emil Jeřábek below, UCC implies the axiom of countable choice for countable sets (the latter abbreviated as CCF).  

*Digging through the paper mentioned by godelian in the comments, I reached [1] in which Howard constructs a model of ZFA in which CCF holds and UCC does not, and by the transfer theorem of Pincus constructs this over ZF. Therefore we have: $$\text{ACC}\Rightarrow\text{UCC}\Rightarrow\text{CCF}$$ The first implication is irreversible in ZFA, by the comment of godelian, and the second irreversible in ZF by [1]. Both papers are two decades old, is there any known progress?
Bibliography:


*

*Howard, P. The axiom of choice for countable collections of countable sets does not imply the countable union theorem. Notre Dame J. Formal Logic Volume 33, Number 2 (1992), 236-243.
 A: The implication $ACC \implies UCC$ is irreversible in $ZF$. This follows again from the transfer theorem of Pincus:

*

*$UCC$ is an injectively boundable statement, see note 103 in "Consequences of the axiom of choice" by Howard & Rubin. Right after the theorem in pp. 285 and its corollary, there are examples of statements of this kind, one of which is form 31 (which is precisely $UCC$). The fact that this is the case follows in turn from the application of lemma 3.5 in Howard, P.-Solski, J.: "The strength of the $\Delta$-system lemma", Notre Dame J. Formal Logic vol 34, pp. 100-106 - 1993


*It is known that $¬ACC$ is boundable, and hence injectively boundable.
Then we can apply the transfer theorem of Pincus to the conjunction $UCC \wedge ¬ACC$ and we are done.
SECOND PROOF: Browsing through the "Consequences..." book I've just found another less direct proof of the same fact. I'm adding it here to avoid the interested person from looking it up for himself (especially since the AC website is not working these days). It involves form 9, known as $W_{\aleph_0}$: a set is finite if and only if it is Dedekind finite. Now, $ACC \implies W_{\aleph_0}$ is provable in $ZF$ (in fact this was already proved by Dedekind), while $UCC$ does not imply $W_{\aleph_0}$. The latter follows from the fact that in the basic Fraenkel model, $\mathcal{N}1$, $UCC$ is valid while $W_{\aleph_0}$ is not, and such a result is transferable by considerations of Pincus that can be found at Pincus, D.: "Zermelo-Fraenkel consistency results by Fraenkel Mostowski methods", J. of Symbolic Logic vol 37, pp. 721-743 - 1972 (doi:10.2307/2272420)
