Metamath Proof Explorer

Theorem aleph1irr

Description: There are at least aleph-one irrationals. (Contributed by NM, 2-Feb-2005)

Ref Expression
Assertion aleph1irr 
|- ( aleph ` 1o ) ~<_ ( RR \ QQ )

Proof

Step Hyp Ref Expression
1 aleph1re 
 |-  ( aleph ` 1o ) ~<_ RR
2 reex 
 |-  RR e. _V
3 numth3 
 |-  ( RR e. _V -> RR e. dom card )
4 2 3 ax-mp 
 |-  RR e. dom card
5 nnenom 
 |-  NN ~~ _om
6 5 ensymi 
 |-  _om ~~ NN
7 ruc 
 |-  NN ~< RR
8 ensdomtr 
 |-  ( ( _om ~~ NN /\ NN ~< RR ) -> _om ~< RR )
9 6 7 8 mp2an 
 |-  _om ~< RR
10 sdomdom 
 |-  ( _om ~< RR -> _om ~<_ RR )
11 9 10 ax-mp 
 |-  _om ~<_ RR
12 resdomq 
 |-  QQ ~< RR
13 infdif 
 |-  ( ( RR e. dom card /\ _om ~<_ RR /\ QQ ~< RR ) -> ( RR \ QQ ) ~~ RR )
14 4 11 12 13 mp3an 
 |-  ( RR \ QQ ) ~~ RR
15 14 ensymi 
 |-  RR ~~ ( RR \ QQ )
16 domentr 
 |-  ( ( ( aleph ` 1o ) ~<_ RR /\ RR ~~ ( RR \ QQ ) ) -> ( aleph ` 1o ) ~<_ ( RR \ QQ ) )
17 1 15 16 mp2an 
 |-  ( aleph ` 1o ) ~<_ ( RR \ QQ )