Metamath Proof Explorer

Theorem gch3

Description: An equivalent formulation of the generalized continuum hypothesis. (Contributed by Mario Carneiro, 15-May-2015)

Ref Expression
Assertion gch3 
|- ( GCH = _V <-> A. x e. On ( aleph ` suc x ) ~~ ~P ( aleph ` x ) )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( GCH = _V /\ x e. On ) -> x e. On )
2 fvex 
 |-  ( aleph ` x ) e. _V
3 simpl 
 |-  ( ( GCH = _V /\ x e. On ) -> GCH = _V )
4 2 3 eleqtrrid 
 |-  ( ( GCH = _V /\ x e. On ) -> ( aleph ` x ) e. GCH )
5 fvex 
 |-  ( aleph ` suc x ) e. _V
6 5 3 eleqtrrid 
 |-  ( ( GCH = _V /\ x e. On ) -> ( aleph ` suc x ) e. GCH )
7 gchaleph2 
 |-  ( ( x e. On /\ ( aleph ` x ) e. GCH /\ ( aleph ` suc x ) e. GCH ) -> ( aleph ` suc x ) ~~ ~P ( aleph ` x ) )
8 1 4 6 7 syl3anc 
 |-  ( ( GCH = _V /\ x e. On ) -> ( aleph ` suc x ) ~~ ~P ( aleph ` x ) )
9 8 ralrimiva 
 |-  ( GCH = _V -> A. x e. On ( aleph ` suc x ) ~~ ~P ( aleph ` x ) )
10 alephgch 
 |-  ( ( aleph ` suc x ) ~~ ~P ( aleph ` x ) -> ( aleph ` x ) e. GCH )
11 10 ralimi 
 |-  ( A. x e. On ( aleph ` suc x ) ~~ ~P ( aleph ` x ) -> A. x e. On ( aleph ` x ) e. GCH )
12 alephfnon 
 |-  aleph Fn On
13 ffnfv 
 |-  ( aleph : On --> GCH <-> ( aleph Fn On /\ A. x e. On ( aleph ` x ) e. GCH ) )
14 12 13 mpbiran 
 |-  ( aleph : On --> GCH <-> A. x e. On ( aleph ` x ) e. GCH )
15 11 14 sylibr 
 |-  ( A. x e. On ( aleph ` suc x ) ~~ ~P ( aleph ` x ) -> aleph : On --> GCH )
16 15 frnd 
 |-  ( A. x e. On ( aleph ` suc x ) ~~ ~P ( aleph ` x ) -> ran aleph C_ GCH )
17 gch2 
 |-  ( GCH = _V <-> ran aleph C_ GCH )
18 16 17 sylibr 
 |-  ( A. x e. On ( aleph ` suc x ) ~~ ~P ( aleph ` x ) -> GCH = _V )
19 9 18 impbii 
 |-  ( GCH = _V <-> A. x e. On ( aleph ` suc x ) ~~ ~P ( aleph ` x ) )