Step |
Hyp |
Ref |
Expression |
1 |
|
alephsucpw2 |
|- -. ~P ( aleph ` A ) ~< ( aleph ` suc A ) |
2 |
|
alephon |
|- ( aleph ` suc A ) e. On |
3 |
|
onenon |
|- ( ( aleph ` suc A ) e. On -> ( aleph ` suc A ) e. dom card ) |
4 |
2 3
|
ax-mp |
|- ( aleph ` suc A ) e. dom card |
5 |
|
simp3 |
|- ( ( A e. On /\ ( aleph ` A ) e. GCH /\ ~P ( aleph ` A ) e. dom card ) -> ~P ( aleph ` A ) e. dom card ) |
6 |
|
domtri2 |
|- ( ( ( aleph ` suc A ) e. dom card /\ ~P ( aleph ` A ) e. dom card ) -> ( ( aleph ` suc A ) ~<_ ~P ( aleph ` A ) <-> -. ~P ( aleph ` A ) ~< ( aleph ` suc A ) ) ) |
7 |
4 5 6
|
sylancr |
|- ( ( A e. On /\ ( aleph ` A ) e. GCH /\ ~P ( aleph ` A ) e. dom card ) -> ( ( aleph ` suc A ) ~<_ ~P ( aleph ` A ) <-> -. ~P ( aleph ` A ) ~< ( aleph ` suc A ) ) ) |
8 |
1 7
|
mpbiri |
|- ( ( A e. On /\ ( aleph ` A ) e. GCH /\ ~P ( aleph ` A ) e. dom card ) -> ( aleph ` suc A ) ~<_ ~P ( aleph ` A ) ) |
9 |
|
fvex |
|- ( aleph ` A ) e. _V |
10 |
|
simp1 |
|- ( ( A e. On /\ ( aleph ` A ) e. GCH /\ ~P ( aleph ` A ) e. dom card ) -> A e. On ) |
11 |
|
alephgeom |
|- ( A e. On <-> _om C_ ( aleph ` A ) ) |
12 |
10 11
|
sylib |
|- ( ( A e. On /\ ( aleph ` A ) e. GCH /\ ~P ( aleph ` A ) e. dom card ) -> _om C_ ( aleph ` A ) ) |
13 |
|
ssdomg |
|- ( ( aleph ` A ) e. _V -> ( _om C_ ( aleph ` A ) -> _om ~<_ ( aleph ` A ) ) ) |
14 |
9 12 13
|
mpsyl |
|- ( ( A e. On /\ ( aleph ` A ) e. GCH /\ ~P ( aleph ` A ) e. dom card ) -> _om ~<_ ( aleph ` A ) ) |
15 |
|
domnsym |
|- ( _om ~<_ ( aleph ` A ) -> -. ( aleph ` A ) ~< _om ) |
16 |
14 15
|
syl |
|- ( ( A e. On /\ ( aleph ` A ) e. GCH /\ ~P ( aleph ` A ) e. dom card ) -> -. ( aleph ` A ) ~< _om ) |
17 |
|
isfinite |
|- ( ( aleph ` A ) e. Fin <-> ( aleph ` A ) ~< _om ) |
18 |
16 17
|
sylnibr |
|- ( ( A e. On /\ ( aleph ` A ) e. GCH /\ ~P ( aleph ` A ) e. dom card ) -> -. ( aleph ` A ) e. Fin ) |
19 |
|
simp2 |
|- ( ( A e. On /\ ( aleph ` A ) e. GCH /\ ~P ( aleph ` A ) e. dom card ) -> ( aleph ` A ) e. GCH ) |
20 |
|
alephordilem1 |
|- ( A e. On -> ( aleph ` A ) ~< ( aleph ` suc A ) ) |
21 |
20
|
3ad2ant1 |
|- ( ( A e. On /\ ( aleph ` A ) e. GCH /\ ~P ( aleph ` A ) e. dom card ) -> ( aleph ` A ) ~< ( aleph ` suc A ) ) |
22 |
|
gchi |
|- ( ( ( aleph ` A ) e. GCH /\ ( aleph ` A ) ~< ( aleph ` suc A ) /\ ( aleph ` suc A ) ~< ~P ( aleph ` A ) ) -> ( aleph ` A ) e. Fin ) |
23 |
22
|
3expia |
|- ( ( ( aleph ` A ) e. GCH /\ ( aleph ` A ) ~< ( aleph ` suc A ) ) -> ( ( aleph ` suc A ) ~< ~P ( aleph ` A ) -> ( aleph ` A ) e. Fin ) ) |
24 |
19 21 23
|
syl2anc |
|- ( ( A e. On /\ ( aleph ` A ) e. GCH /\ ~P ( aleph ` A ) e. dom card ) -> ( ( aleph ` suc A ) ~< ~P ( aleph ` A ) -> ( aleph ` A ) e. Fin ) ) |
25 |
18 24
|
mtod |
|- ( ( A e. On /\ ( aleph ` A ) e. GCH /\ ~P ( aleph ` A ) e. dom card ) -> -. ( aleph ` suc A ) ~< ~P ( aleph ` A ) ) |
26 |
|
domtri2 |
|- ( ( ~P ( aleph ` A ) e. dom card /\ ( aleph ` suc A ) e. dom card ) -> ( ~P ( aleph ` A ) ~<_ ( aleph ` suc A ) <-> -. ( aleph ` suc A ) ~< ~P ( aleph ` A ) ) ) |
27 |
5 4 26
|
sylancl |
|- ( ( A e. On /\ ( aleph ` A ) e. GCH /\ ~P ( aleph ` A ) e. dom card ) -> ( ~P ( aleph ` A ) ~<_ ( aleph ` suc A ) <-> -. ( aleph ` suc A ) ~< ~P ( aleph ` A ) ) ) |
28 |
25 27
|
mpbird |
|- ( ( A e. On /\ ( aleph ` A ) e. GCH /\ ~P ( aleph ` A ) e. dom card ) -> ~P ( aleph ` A ) ~<_ ( aleph ` suc A ) ) |
29 |
|
sbth |
|- ( ( ( aleph ` suc A ) ~<_ ~P ( aleph ` A ) /\ ~P ( aleph ` A ) ~<_ ( aleph ` suc A ) ) -> ( aleph ` suc A ) ~~ ~P ( aleph ` A ) ) |
30 |
8 28 29
|
syl2anc |
|- ( ( A e. On /\ ( aleph ` A ) e. GCH /\ ~P ( aleph ` A ) e. dom card ) -> ( aleph ` suc A ) ~~ ~P ( aleph ` A ) ) |