Metamath Proof Explorer

Theorem gch2

Description: It is sufficient to require that all alephs are GCH-sets to ensure the full generalized continuum hypothesis. (The proof uses the Axiom of Regularity.) (Contributed by Mario Carneiro, 15-May-2015)

Ref Expression
Assertion gch2 ⊢GCH=V↔ran⁡ℵ⊆GCH

Proof

Step Hyp Ref Expression
1 ssv ⊢ran⁡ℵ⊆V
2 sseq2 ⊢GCH=V→ran⁡ℵ⊆GCH↔ran⁡ℵ⊆V
3 1 2 mpbiri ⊢GCH=V→ran⁡ℵ⊆GCH
4 cardidm ⊢card⁡card⁡x=card⁡x
5 iscard3 ⊢card⁡card⁡x=card⁡x↔card⁡x∈ω∪ran⁡ℵ
6 4 5 mpbi ⊢card⁡x∈ω∪ran⁡ℵ
7 elun ⊢card⁡x∈ω∪ran⁡ℵ↔card⁡x∈ω∨card⁡x∈ran⁡ℵ
8 6 7 mpbi ⊢card⁡x∈ω∨card⁡x∈ran⁡ℵ
9 fingch ⊢Fin⊆GCH
10 nnfi ⊢card⁡x∈ω→card⁡x∈Fin
11 9 10 sselid ⊢card⁡x∈ω→card⁡x∈GCH
12 11 a1i ⊢ran⁡ℵ⊆GCH→card⁡x∈ω→card⁡x∈GCH
13 ssel ⊢ran⁡ℵ⊆GCH→card⁡x∈ran⁡ℵ→card⁡x∈GCH
14 12 13 jaod ⊢ran⁡ℵ⊆GCH→card⁡x∈ω∨card⁡x∈ran⁡ℵ→card⁡x∈GCH
15 8 14 mpi ⊢ran⁡ℵ⊆GCH→card⁡x∈GCH
16 vex ⊢x∈V
17 alephon ⊢ℵ⁡suc⁡x∈On
18 simpr ⊢ran⁡ℵ⊆GCH∧x∈On→x∈On
19 simpl ⊢ran⁡ℵ⊆GCH∧x∈On→ran⁡ℵ⊆GCH
20 alephfnon ⊢ℵFnOn
21 fnfvelrn ⊢ℵFnOn∧x∈On→ℵ⁡x∈ran⁡ℵ
22 20 18 21 sylancr ⊢ran⁡ℵ⊆GCH∧x∈On→ℵ⁡x∈ran⁡ℵ
23 19 22 sseldd ⊢ran⁡ℵ⊆GCH∧x∈On→ℵ⁡x∈GCH
24 onsuc ⊢x∈On→suc⁡x∈On
25 24 adantl ⊢ran⁡ℵ⊆GCH∧x∈On→suc⁡x∈On
26 fnfvelrn ⊢ℵFnOn∧suc⁡x∈On→ℵ⁡suc⁡x∈ran⁡ℵ
27 20 25 26 sylancr ⊢ran⁡ℵ⊆GCH∧x∈On→ℵ⁡suc⁡x∈ran⁡ℵ
28 19 27 sseldd ⊢ran⁡ℵ⊆GCH∧x∈On→ℵ⁡suc⁡x∈GCH
29 gchaleph2 ⊢x∈On∧ℵ⁡x∈GCH∧ℵ⁡suc⁡x∈GCH→ℵ⁡suc⁡x≈𝒫ℵ⁡x
30 18 23 28 29 syl3anc ⊢ran⁡ℵ⊆GCH∧x∈On→ℵ⁡suc⁡x≈𝒫ℵ⁡x
31 isnumi ⊢ℵ⁡suc⁡x∈On∧ℵ⁡suc⁡x≈𝒫ℵ⁡x→𝒫ℵ⁡x∈dom⁡card
32 17 30 31 sylancr ⊢ran⁡ℵ⊆GCH∧x∈On→𝒫ℵ⁡x∈dom⁡card
33 32 ralrimiva ⊢ran⁡ℵ⊆GCH→∀x∈On𝒫ℵ⁡x∈dom⁡card
34 dfac12 ⊢CHOICE↔∀x∈On𝒫ℵ⁡x∈dom⁡card
35 33 34 sylibr ⊢ran⁡ℵ⊆GCH→CHOICE
36 dfac10 ⊢CHOICE↔dom⁡card=V
37 35 36 sylib ⊢ran⁡ℵ⊆GCH→dom⁡card=V
38 16 37 eleqtrrid ⊢ran⁡ℵ⊆GCH→x∈dom⁡card
39 cardid2 ⊢x∈dom⁡card→card⁡x≈x
40 engch ⊢card⁡x≈x→card⁡x∈GCH↔x∈GCH
41 38 39 40 3syl ⊢ran⁡ℵ⊆GCH→card⁡x∈GCH↔x∈GCH
42 15 41 mpbid ⊢ran⁡ℵ⊆GCH→x∈GCH
43 16 a1i ⊢ran⁡ℵ⊆GCH→x∈V
44 42 43 2thd ⊢ran⁡ℵ⊆GCH→x∈GCH↔x∈V
45 44 eqrdv ⊢ran⁡ℵ⊆GCH→GCH=V
46 3 45 impbii ⊢GCH=V↔ran⁡ℵ⊆GCH