Metamath Proof Explorer


Theorem gchaleph2

Description: If ( alephA ) and ( alephsuc A ) are GCH-sets, then the successor aleph ( alephsuc A ) is equinumerous to the powerset of ( alephA ) . (Contributed by Mario Carneiro, 31-May-2015)

Ref Expression
Assertion gchaleph2
|- ( ( A e. On /\ ( aleph ` A ) e. GCH /\ ( aleph ` suc A ) e. GCH ) -> ( aleph ` suc A ) ~~ ~P ( aleph ` A ) )

Proof

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