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
|- QQ ~~ _om

Proof

Step Hyp Ref Expression
1 qnnen
 |-  QQ ~~ NN
2 nnenom
 |-  NN ~~ _om
3 1 2 entri
 |-  QQ ~~ _om