Metamath Proof Explorer

Theorem qnnen

Description: The rational numbers are countable. This proof does not use the Axiom of Choice, even though it uses an onto function, because the base set ( ZZ X. NN ) is numerable. Exercise 2 of Enderton p. 133. For purposes of the Metamath 100 list, we are considering Mario Carneiro's revision as the date this proof was completed. This is Metamath 100 proof #3. (Contributed by NM, 31-Jul-2004) (Revised by Mario Carneiro, 3-Mar-2013)

Ref Expression
Assertion qnnen 
|- QQ ~~ NN

Proof

Step Hyp Ref Expression
1 omelon 
 |-  _om e. On
2 nnenom 
 |-  NN ~~ _om
3 2 ensymi 
 |-  _om ~~ NN
4 isnumi 
 |-  ( ( _om e. On /\ _om ~~ NN ) -> NN e. dom card )
5 1 3 4 mp2an 
 |-  NN e. dom card
6 znnen 
 |-  ZZ ~~ NN
7 ennum 
 |-  ( ZZ ~~ NN -> ( ZZ e. dom card <-> NN e. dom card ) )
8 6 7 ax-mp 
 |-  ( ZZ e. dom card <-> NN e. dom card )
9 5 8 mpbir 
 |-  ZZ e. dom card
10 xpnum 
 |-  ( ( ZZ e. dom card /\ NN e. dom card ) -> ( ZZ X. NN ) e. dom card )
11 9 5 10 mp2an 
 |-  ( ZZ X. NN ) e. dom card
12 eqid 
 |-  ( x e. ZZ , y e. NN |-> ( x / y ) ) = ( x e. ZZ , y e. NN |-> ( x / y ) )
13 ovex 
 |-  ( x / y ) e. _V
14 12 13 fnmpoi 
 |-  ( x e. ZZ , y e. NN |-> ( x / y ) ) Fn ( ZZ X. NN )
15 12 rnmpo 
 |-  ran ( x e. ZZ , y e. NN |-> ( x / y ) ) = { z | E. x e. ZZ E. y e. NN z = ( x / y ) }
16 elq 
 |-  ( z e. QQ <-> E. x e. ZZ E. y e. NN z = ( x / y ) )
17 16 abbi2i 
 |-  QQ = { z | E. x e. ZZ E. y e. NN z = ( x / y ) }
18 15 17 eqtr4i 
 |-  ran ( x e. ZZ , y e. NN |-> ( x / y ) ) = QQ
19 df-fo 
 |-  ( ( x e. ZZ , y e. NN |-> ( x / y ) ) : ( ZZ X. NN ) -onto-> QQ <-> ( ( x e. ZZ , y e. NN |-> ( x / y ) ) Fn ( ZZ X. NN ) /\ ran ( x e. ZZ , y e. NN |-> ( x / y ) ) = QQ ) )
20 14 18 19 mpbir2an 
 |-  ( x e. ZZ , y e. NN |-> ( x / y ) ) : ( ZZ X. NN ) -onto-> QQ
21 fodomnum 
 |-  ( ( ZZ X. NN ) e. dom card -> ( ( x e. ZZ , y e. NN |-> ( x / y ) ) : ( ZZ X. NN ) -onto-> QQ -> QQ ~<_ ( ZZ X. NN ) ) )
22 11 20 21 mp2 
 |-  QQ ~<_ ( ZZ X. NN )
23 nnex 
 |-  NN e. _V
24 23 enref 
 |-  NN ~~ NN
25 xpen 
 |-  ( ( ZZ ~~ NN /\ NN ~~ NN ) -> ( ZZ X. NN ) ~~ ( NN X. NN ) )
26 6 24 25 mp2an 
 |-  ( ZZ X. NN ) ~~ ( NN X. NN )
27 xpnnen 
 |-  ( NN X. NN ) ~~ NN
28 26 27 entri 
 |-  ( ZZ X. NN ) ~~ NN
29 domentr 
 |-  ( ( QQ ~<_ ( ZZ X. NN ) /\ ( ZZ X. NN ) ~~ NN ) -> QQ ~<_ NN )
30 22 28 29 mp2an 
 |-  QQ ~<_ NN
31 qex 
 |-  QQ e. _V
32 nnssq 
 |-  NN C_ QQ
33 ssdomg 
 |-  ( QQ e. _V -> ( NN C_ QQ -> NN ~<_ QQ ) )
34 31 32 33 mp2 
 |-  NN ~<_ QQ
35 sbth 
 |-  ( ( QQ ~<_ NN /\ NN ~<_ QQ ) -> QQ ~~ NN )
36 30 34 35 mp2an 
 |-  QQ ~~ NN