Metamath Proof Explorer

Theorem alephgch

Description: If ( alephsuc A ) is equinumerous to the powerset of ( alephA ) , then ( alephA ) is a GCH-set. (Contributed by Mario Carneiro, 15-May-2015)

Ref Expression
Assertion alephgch 
|- ( ( aleph ` suc A ) ~~ ~P ( aleph ` A ) -> ( aleph ` A ) e. GCH )

Proof

Step Hyp Ref Expression
1 alephnbtwn2 
 |-  -. ( ( aleph ` A ) ~< x /\ x ~< ( aleph ` suc A ) )
2 sdomen2 
 |-  ( ( aleph ` suc A ) ~~ ~P ( aleph ` A ) -> ( x ~< ( aleph ` suc A ) <-> x ~< ~P ( aleph ` A ) ) )
3 2 anbi2d 
 |-  ( ( aleph ` suc A ) ~~ ~P ( aleph ` A ) -> ( ( ( aleph ` A ) ~< x /\ x ~< ( aleph ` suc A ) ) <-> ( ( aleph ` A ) ~< x /\ x ~< ~P ( aleph ` A ) ) ) )
4 1 3 mtbii 
 |-  ( ( aleph ` suc A ) ~~ ~P ( aleph ` A ) -> -. ( ( aleph ` A ) ~< x /\ x ~< ~P ( aleph ` A ) ) )
5 4 alrimiv 
 |-  ( ( aleph ` suc A ) ~~ ~P ( aleph ` A ) -> A. x -. ( ( aleph ` A ) ~< x /\ x ~< ~P ( aleph ` A ) ) )
6 5 olcd 
 |-  ( ( aleph ` suc A ) ~~ ~P ( aleph ` A ) -> ( ( aleph ` A ) e. Fin \/ A. x -. ( ( aleph ` A ) ~< x /\ x ~< ~P ( aleph ` A ) ) ) )
7 fvex 
 |-  ( aleph ` A ) e. _V
8 elgch 
 |-  ( ( aleph ` A ) e. _V -> ( ( aleph ` A ) e. GCH <-> ( ( aleph ` A ) e. Fin \/ A. x -. ( ( aleph ` A ) ~< x /\ x ~< ~P ( aleph ` A ) ) ) ) )
9 7 8 ax-mp 
 |-  ( ( aleph ` A ) e. GCH <-> ( ( aleph ` A ) e. Fin \/ A. x -. ( ( aleph ` A ) ~< x /\ x ~< ~P ( aleph ` A ) ) ) )
10 6 9 sylibr 
 |-  ( ( aleph ` suc A ) ~~ ~P ( aleph ` A ) -> ( aleph ` A ) e. GCH )