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 ↔ ∀ x ∈ On ℵ ⁡ suc ⁡ x ≈ 𝒫 ℵ ⁡ x

Proof

Step Hyp Ref Expression
1 simpr ⊢ GCH = V ∧ x ∈ On → x ∈ On
2 fvex ⊢ ℵ ⁡ x ∈ V
3 simpl ⊢ GCH = V ∧ x ∈ On → GCH = V
4 2 3 eleqtrrid ⊢ GCH = V ∧ x ∈ On → ℵ ⁡ x ∈ GCH
5 fvex ⊢ ℵ ⁡ suc ⁡ x ∈ V
6 5 3 eleqtrrid ⊢ GCH = V ∧ x ∈ On → ℵ ⁡ suc ⁡ x ∈ GCH
7 gchaleph2 ⊢ x ∈ On ∧ ℵ ⁡ x ∈ GCH ∧ ℵ ⁡ suc ⁡ x ∈ GCH → ℵ ⁡ suc ⁡ x ≈ 𝒫 ℵ ⁡ x
8 1 4 6 7 syl3anc ⊢ GCH = V ∧ x ∈ On → ℵ ⁡ suc ⁡ x ≈ 𝒫 ℵ ⁡ x
9 8 ralrimiva ⊢ GCH = V → ∀ x ∈ On ℵ ⁡ suc ⁡ x ≈ 𝒫 ℵ ⁡ x
10 alephgch ⊢ ℵ ⁡ suc ⁡ x ≈ 𝒫 ℵ ⁡ x → ℵ ⁡ x ∈ GCH
11 10 ralimi ⊢ ∀ x ∈ On ℵ ⁡ suc ⁡ x ≈ 𝒫 ℵ ⁡ x → ∀ x ∈ On ℵ ⁡ x ∈ GCH
12 alephfnon ⊢ ℵ Fn On
13 ffnfv ⊢ ℵ : On ⟶ GCH ↔ ℵ Fn On ∧ ∀ x ∈ On ℵ ⁡ x ∈ GCH
14 12 13 mpbiran ⊢ ℵ : On ⟶ GCH ↔ ∀ x ∈ On ℵ ⁡ x ∈ GCH
15 11 14 sylibr ⊢ ∀ x ∈ On ℵ ⁡ suc ⁡ x ≈ 𝒫 ℵ ⁡ x → ℵ : On ⟶ GCH
16 15 frnd ⊢ ∀ x ∈ On ℵ ⁡ suc ⁡ x ≈ 𝒫 ℵ ⁡ x → ran ⁡ ℵ ⊆ GCH
17 gch2 ⊢ GCH = V ↔ ran ⁡ ℵ ⊆ GCH
18 16 17 sylibr ⊢ ∀ x ∈ On ℵ ⁡ suc ⁡ x ≈ 𝒫 ℵ ⁡ x → GCH = V
19 9 18 impbii ⊢ GCH = V ↔ ∀ x ∈ On ℵ ⁡ suc ⁡ x ≈ 𝒫 ℵ ⁡ x