This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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