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 ⊢ ℵ Fn On
21 fnfvelrn ⊢ ℵ Fn On ∧ 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 ⊢ ℵ Fn On ∧ 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