Step |
Hyp |
Ref |
Expression |
1 |
|
aleph0 |
|- ( aleph ` (/) ) = _om |
2 |
|
0ss |
|- (/) C_ A |
3 |
|
0elon |
|- (/) e. On |
4 |
|
alephord3 |
|- ( ( (/) e. On /\ A e. On ) -> ( (/) C_ A <-> ( aleph ` (/) ) C_ ( aleph ` A ) ) ) |
5 |
3 4
|
mpan |
|- ( A e. On -> ( (/) C_ A <-> ( aleph ` (/) ) C_ ( aleph ` A ) ) ) |
6 |
2 5
|
mpbii |
|- ( A e. On -> ( aleph ` (/) ) C_ ( aleph ` A ) ) |
7 |
1 6
|
eqsstrrid |
|- ( A e. On -> _om C_ ( aleph ` A ) ) |
8 |
|
peano1 |
|- (/) e. _om |
9 |
|
ordom |
|- Ord _om |
10 |
|
ord0 |
|- Ord (/) |
11 |
|
ordtri1 |
|- ( ( Ord _om /\ Ord (/) ) -> ( _om C_ (/) <-> -. (/) e. _om ) ) |
12 |
9 10 11
|
mp2an |
|- ( _om C_ (/) <-> -. (/) e. _om ) |
13 |
12
|
con2bii |
|- ( (/) e. _om <-> -. _om C_ (/) ) |
14 |
8 13
|
mpbi |
|- -. _om C_ (/) |
15 |
|
ndmfv |
|- ( -. A e. dom aleph -> ( aleph ` A ) = (/) ) |
16 |
15
|
sseq2d |
|- ( -. A e. dom aleph -> ( _om C_ ( aleph ` A ) <-> _om C_ (/) ) ) |
17 |
14 16
|
mtbiri |
|- ( -. A e. dom aleph -> -. _om C_ ( aleph ` A ) ) |
18 |
17
|
con4i |
|- ( _om C_ ( aleph ` A ) -> A e. dom aleph ) |
19 |
|
alephfnon |
|- aleph Fn On |
20 |
19
|
fndmi |
|- dom aleph = On |
21 |
18 20
|
eleqtrdi |
|- ( _om C_ ( aleph ` A ) -> A e. On ) |
22 |
7 21
|
impbii |
|- ( A e. On <-> _om C_ ( aleph ` A ) ) |