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=VxOnsucx𝒫x

Proof

Step Hyp Ref Expression
1 simpr GCH=VxOnxOn
2 fvex xV
3 simpl GCH=VxOnGCH=V
4 2 3 eleqtrrid GCH=VxOnxGCH
5 fvex sucxV
6 5 3 eleqtrrid GCH=VxOnsucxGCH
7 gchaleph2 xOnxGCHsucxGCHsucx𝒫x
8 1 4 6 7 syl3anc GCH=VxOnsucx𝒫x
9 8 ralrimiva GCH=VxOnsucx𝒫x
10 alephgch sucx𝒫xxGCH
11 10 ralimi xOnsucx𝒫xxOnxGCH
12 alephfnon FnOn
13 ffnfv :OnGCHFnOnxOnxGCH
14 12 13 mpbiran :OnGCHxOnxGCH
15 11 14 sylibr xOnsucx𝒫x:OnGCH
16 15 frnd xOnsucx𝒫xranGCH
17 gch2 GCH=VranGCH
18 16 17 sylibr xOnsucx𝒫xGCH=V
19 9 18 impbii GCH=VxOnsucx𝒫x