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