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 ω