This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝑥 ) ≈ 𝒫 ( ℵ ‘ 𝑥 ) )