Step |
Hyp |
Ref |
Expression |
1 |
|
harcl |
|- ( har ` ( aleph ` A ) ) e. On |
2 |
|
alephon |
|- ( aleph ` A ) e. On |
3 |
|
onenon |
|- ( ( aleph ` A ) e. On -> ( aleph ` A ) e. dom card ) |
4 |
|
harsdom |
|- ( ( aleph ` A ) e. dom card -> ( aleph ` A ) ~< ( har ` ( aleph ` A ) ) ) |
5 |
2 3 4
|
mp2b |
|- ( aleph ` A ) ~< ( har ` ( aleph ` A ) ) |
6 |
|
simp1 |
|- ( ( A e. On /\ ( aleph ` A ) e. GCH /\ ( aleph ` suc A ) e. GCH ) -> A e. On ) |
7 |
|
alephgeom |
|- ( A e. On <-> _om C_ ( aleph ` A ) ) |
8 |
6 7
|
sylib |
|- ( ( A e. On /\ ( aleph ` A ) e. GCH /\ ( aleph ` suc A ) e. GCH ) -> _om C_ ( aleph ` A ) ) |
9 |
|
ssdomg |
|- ( ( aleph ` A ) e. On -> ( _om C_ ( aleph ` A ) -> _om ~<_ ( aleph ` A ) ) ) |
10 |
2 8 9
|
mpsyl |
|- ( ( A e. On /\ ( aleph ` A ) e. GCH /\ ( aleph ` suc A ) e. GCH ) -> _om ~<_ ( aleph ` A ) ) |
11 |
|
simp2 |
|- ( ( A e. On /\ ( aleph ` A ) e. GCH /\ ( aleph ` suc A ) e. GCH ) -> ( aleph ` A ) e. GCH ) |
12 |
|
alephsuc |
|- ( A e. On -> ( aleph ` suc A ) = ( har ` ( aleph ` A ) ) ) |
13 |
6 12
|
syl |
|- ( ( A e. On /\ ( aleph ` A ) e. GCH /\ ( aleph ` suc A ) e. GCH ) -> ( aleph ` suc A ) = ( har ` ( aleph ` A ) ) ) |
14 |
|
simp3 |
|- ( ( A e. On /\ ( aleph ` A ) e. GCH /\ ( aleph ` suc A ) e. GCH ) -> ( aleph ` suc A ) e. GCH ) |
15 |
13 14
|
eqeltrrd |
|- ( ( A e. On /\ ( aleph ` A ) e. GCH /\ ( aleph ` suc A ) e. GCH ) -> ( har ` ( aleph ` A ) ) e. GCH ) |
16 |
|
gchpwdom |
|- ( ( _om ~<_ ( aleph ` A ) /\ ( aleph ` A ) e. GCH /\ ( har ` ( aleph ` A ) ) e. GCH ) -> ( ( aleph ` A ) ~< ( har ` ( aleph ` A ) ) <-> ~P ( aleph ` A ) ~<_ ( har ` ( aleph ` A ) ) ) ) |
17 |
10 11 15 16
|
syl3anc |
|- ( ( A e. On /\ ( aleph ` A ) e. GCH /\ ( aleph ` suc A ) e. GCH ) -> ( ( aleph ` A ) ~< ( har ` ( aleph ` A ) ) <-> ~P ( aleph ` A ) ~<_ ( har ` ( aleph ` A ) ) ) ) |
18 |
5 17
|
mpbii |
|- ( ( A e. On /\ ( aleph ` A ) e. GCH /\ ( aleph ` suc A ) e. GCH ) -> ~P ( aleph ` A ) ~<_ ( har ` ( aleph ` A ) ) ) |
19 |
|
ondomen |
|- ( ( ( har ` ( aleph ` A ) ) e. On /\ ~P ( aleph ` A ) ~<_ ( har ` ( aleph ` A ) ) ) -> ~P ( aleph ` A ) e. dom card ) |
20 |
1 18 19
|
sylancr |
|- ( ( A e. On /\ ( aleph ` A ) e. GCH /\ ( aleph ` suc A ) e. GCH ) -> ~P ( aleph ` A ) e. dom card ) |
21 |
|
gchaleph |
|- ( ( A e. On /\ ( aleph ` A ) e. GCH /\ ~P ( aleph ` A ) e. dom card ) -> ( aleph ` suc A ) ~~ ~P ( aleph ` A ) ) |
22 |
20 21
|
syld3an3 |
|- ( ( A e. On /\ ( aleph ` A ) e. GCH /\ ( aleph ` suc A ) e. GCH ) -> ( aleph ` suc A ) ~~ ~P ( aleph ` A ) ) |