= Countable union of explicitly ordered finite lists without choice
Given finite lists $\ell_0,\ell_1,\ldots$ in a <set> $X$, their union of entries has an explicit enumeration from a subset of $\mathbb N^2$: use the existing positions in each list and a <Cantor pairing function>. If the union is infinite, successively take the first occurrence of an entry not previously taken, in the order of its natural-number code. The <well-order> on <natural numbers> makes each step uniquely determined and yields an injection $\mathbb N\to X$. No <axiom of choice> is needed. This does not assert that an arbitrary countable family of unordered <finite sets> has a countable union in <ZF> without the <axiom of choice>.
Back to article page
