Metamath Proof Explorer


Theorem qenom

Description: The set of rational numbers is equinumerous to omega (the set of finite ordinal numbers). (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Assertion qenom ℚ ≈ ω

Proof

Step Hyp Ref Expression
1 qnnen ℚ ≈ ℕ
2 nnenom ℕ ≈ ω
3 1 2 entri ℚ ≈ ω