Solution (source code)

= Solution

A <set> is <countable> if it is finite or admits an <injection> into the natural numbers; an infinite <countable set> can equivalently be listed as a sequence. Let $A=\bigcup_{i\ge1}A_i$ with each $A_i$ <countable>. Choose an enumeration of each nonempty $A_i$, allowing repetition if it is finite. List the pairs $(i,j)\in\mathbb N^2$ in successive finite diagonals of constant $i+j$ and output the $j$th member of $A_i$. This lists every member of $A$, so $A$ is <countable>; empty sets contribute nothing, and repetitions can be removed by retaining first occurrences. This is the <countable union of countable sets> theorem, in the usual setting with <axiom of countable choice> for selecting the enumerations.

Each positive-length interval $J_i$ has a nonempty interior containing a <rational number> by the <density of the rational numbers>. Fix one enumeration of the <rational numbers> and let $q_i$ be its first member in the interior of $J_i$. Disjointness gives $i\ne j\Rightarrow q_i\ne q_j$, so $i\mapsto q_i$ is an <injection> of $I$ into a <countable set>. Hence $I$ is <countable>. This proof of the <countability of disjoint positive-length intervals> uses a fixed enumeration and needs no arbitrary simultaneous choice of rationals.