| 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 |