Metamath Proof Explorer

Theorem ruc

Description: The set of positive integers is strictly dominated by the set of real numbers, i.e. the real numbers are uncountable. The proof consists of lemmas ruclem1 through ruclem13 and this final piece. Our proof is based on the proof of Theorem 5.18 of Truss p. 114. See ruclem13 for the function existence version of this theorem. For an informal discussion of this proof, see mmcomplex.html#uncountable . For an alternate proof see rucALT . This is Metamath 100 proof #22. (Contributed by NM, 13-Oct-2004)

Ref Expression
Assertion ruc 
|- NN ~< RR

Proof

Step Hyp Ref Expression
1 reex 
 |-  RR e. _V
2 nnssre 
 |-  NN C_ RR
3 ssdomg 
 |-  ( RR e. _V -> ( NN C_ RR -> NN ~<_ RR ) )
4 1 2 3 mp2 
 |-  NN ~<_ RR
5 ruclem13 
 |-  -. f : NN -onto-> RR
6 f1ofo 
 |-  ( f : NN -1-1-onto-> RR -> f : NN -onto-> RR )
7 5 6 mto 
 |-  -. f : NN -1-1-onto-> RR
8 7 nex 
 |-  -. E. f f : NN -1-1-onto-> RR
9 bren 
 |-  ( NN ~~ RR <-> E. f f : NN -1-1-onto-> RR )
10 8 9 mtbir 
 |-  -. NN ~~ RR
11 brsdom 
 |-  ( NN ~< RR <-> ( NN ~<_ RR /\ -. NN ~~ RR ) )
12 4 10 11 mpbir2an 
 |-  NN ~< RR