$\mathbb{Q}$ is countably infinite

$\mathbb{Q}\approx \mathbb{N}$ (Equinumerous sets, $A\approx B$ and $A⪯B$): the rationals are countably infinite (Finite, countably infinite, countable, uncountable).

No choice principle is used. The one place where a reader expects a choice, "pick a representative $a\mathrm{/}b$ of each rational", is exactly where Every rational has a positive-denominator representative applies: every rational has a representative with positive denominator, so the map $(a,b)\mapsto [(a,b)]$ defined on $\mathbb{Z}\times {\mathbb{Z}}_{>0}$ is already surjective onto $\mathbb{Q}$, and countability follows from a surjection without ever selecting a representative. The same device handles $\mathbb{Z}$, which is a surjective image of $\mathbb{N}\times \mathbb{N}$ by construction (The integers as equivalence classes of pairs of naturals).

• Why Schröder-Bernstein rather than a count. The usual last line is "countable, and infinite because $\mathbb{N}$ injects into it". Turning that into a proof requires knowing that a set containing an injective copy of $\mathbb{N}$ is not finite, which is the pigeonhole principle, The pigeonhole principle on $\mathbb{N}$, proved earlier on this page. That route is now available, but it is a detour: The Schröder-Bernstein theorem gets the bijection directly from the two injections already in hand, and it is choice free, so nothing is lost.

• Lowest terms are not needed and are not available. A frequent presentation injects $\mathbb{Q}$ into $\mathbb{Z}\times \mathbb{N}$ by sending each rational to its representative in lowest terms. That map needs greatest common divisors, which are not available at this point in the reading order; they are developed later on the divisibility-and-GCD page. Working with a surjection instead of an injection avoids that later dependency. Working with a surjection instead of an injection avoids the issue entirely: repetitions in an enumeration are harmless (A nonempty set is at most countable iff it is a surjective image of $\mathbb{N}$).

• The proof shows in passing that $\mathbb{Z}\approx \mathbb{N}$, by the same two-injection argument applied to [L7] and step 1.1, and that $\mathbb{Q}\times \mathbb{Q}$, ${\mathbb{Q}}^3$ and so on are countable (A product of two at most countable sets is at most countable). The contrast with $\mathbb{R}$ is uncountable (Cantor's nested intervals, 1874) is the point of the page: adding all limits of rational approximations to $\mathbb{Q}$ changes the size of the set, not merely its arithmetic.