Metamath Proof Explorer

Theorem aleph1re

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

Ref Expression
Assertion aleph1re 
|- ( aleph ` 1o ) ~<_ RR

Proof

Step Hyp Ref Expression
1 aleph0 
 |-  ( aleph ` (/) ) = _om
2 nnenom 
 |-  NN ~~ _om
3 2 ensymi 
 |-  _om ~~ NN
4 1 3 eqbrtri 
 |-  ( aleph ` (/) ) ~~ NN
5 ruc 
 |-  NN ~< RR
6 ensdomtr 
 |-  ( ( ( aleph ` (/) ) ~~ NN /\ NN ~< RR ) -> ( aleph ` (/) ) ~< RR )
7 4 5 6 mp2an 
 |-  ( aleph ` (/) ) ~< RR
8 alephnbtwn2 
 |-  -. ( ( aleph ` (/) ) ~< RR /\ RR ~< ( aleph ` suc (/) ) )
9 7 8 mptnan 
 |-  -. RR ~< ( aleph ` suc (/) )
10 df-1o 
 |-  1o = suc (/)
11 10 fveq2i 
 |-  ( aleph ` 1o ) = ( aleph ` suc (/) )
12 11 breq2i 
 |-  ( RR ~< ( aleph ` 1o ) <-> RR ~< ( aleph ` suc (/) ) )
13 9 12 mtbir 
 |-  -. RR ~< ( aleph ` 1o )
14 fvex 
 |-  ( aleph ` 1o ) e. _V
15 reex 
 |-  RR e. _V
16 domtri 
 |-  ( ( ( aleph ` 1o ) e. _V /\ RR e. _V ) -> ( ( aleph ` 1o ) ~<_ RR <-> -. RR ~< ( aleph ` 1o ) ) )
17 14 15 16 mp2an 
 |-  ( ( aleph ` 1o ) ~<_ RR <-> -. RR ~< ( aleph ` 1o ) )
18 13 17 mpbir 
 |-  ( aleph ` 1o ) ~<_ RR