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 ↔ ∀ 𝑥 ∈ On ( ℵ ‘ suc 𝑥 ) ≈ 𝒫 ( ℵ ‘ 𝑥 ) )

Proof

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