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