Metamath Proof Explorer

Theorem gchaleph

Description: If ( alephA ) is a GCH-set and its powerset is well-orderable, then the successor aleph ( alephsuc A ) is equinumerous to the powerset of ( alephA ) . (Contributed by Mario Carneiro, 15-May-2015)

Ref Expression
Assertion gchaleph ⊢ A ∈ On ∧ ℵ ⁡ A ∈ GCH ∧ 𝒫 ℵ ⁡ A ∈ dom ⁡ card → ℵ ⁡ suc ⁡ A ≈ 𝒫 ℵ ⁡ A

Proof

Step Hyp Ref Expression
1 alephsucpw2 ⊢ ¬ 𝒫 ℵ ⁡ A ≺ ℵ ⁡ suc ⁡ A
2 alephon ⊢ ℵ ⁡ suc ⁡ A ∈ On
3 onenon ⊢ ℵ ⁡ suc ⁡ A ∈ On → ℵ ⁡ suc ⁡ A ∈ dom ⁡ card
4 2 3 ax-mp ⊢ ℵ ⁡ suc ⁡ A ∈ dom ⁡ card
5 simp3 ⊢ A ∈ On ∧ ℵ ⁡ A ∈ GCH ∧ 𝒫 ℵ ⁡ A ∈ dom ⁡ card → 𝒫 ℵ ⁡ A ∈ dom ⁡ card
6 domtri2 ⊢ ℵ ⁡ suc ⁡ A ∈ dom ⁡ card ∧ 𝒫 ℵ ⁡ A ∈ dom ⁡ card → ℵ ⁡ suc ⁡ A ≼ 𝒫 ℵ ⁡ A ↔ ¬ 𝒫 ℵ ⁡ A ≺ ℵ ⁡ suc ⁡ A
7 4 5 6 sylancr ⊢ A ∈ On ∧ ℵ ⁡ A ∈ GCH ∧ 𝒫 ℵ ⁡ A ∈ dom ⁡ card → ℵ ⁡ suc ⁡ A ≼ 𝒫 ℵ ⁡ A ↔ ¬ 𝒫 ℵ ⁡ A ≺ ℵ ⁡ suc ⁡ A
8 1 7 mpbiri ⊢ A ∈ On ∧ ℵ ⁡ A ∈ GCH ∧ 𝒫 ℵ ⁡ A ∈ dom ⁡ card → ℵ ⁡ suc ⁡ A ≼ 𝒫 ℵ ⁡ A
9 fvex ⊢ ℵ ⁡ A ∈ V
10 simp1 ⊢ A ∈ On ∧ ℵ ⁡ A ∈ GCH ∧ 𝒫 ℵ ⁡ A ∈ dom ⁡ card → A ∈ On
11 alephgeom ⊢ A ∈ On ↔ ω ⊆ ℵ ⁡ A
12 10 11 sylib ⊢ A ∈ On ∧ ℵ ⁡ A ∈ GCH ∧ 𝒫 ℵ ⁡ A ∈ dom ⁡ card → ω ⊆ ℵ ⁡ A
13 ssdomg ⊢ ℵ ⁡ A ∈ V → ω ⊆ ℵ ⁡ A → ω ≼ ℵ ⁡ A
14 9 12 13 mpsyl ⊢ A ∈ On ∧ ℵ ⁡ A ∈ GCH ∧ 𝒫 ℵ ⁡ A ∈ dom ⁡ card → ω ≼ ℵ ⁡ A
15 domnsym ⊢ ω ≼ ℵ ⁡ A → ¬ ℵ ⁡ A ≺ ω
16 14 15 syl ⊢ A ∈ On ∧ ℵ ⁡ A ∈ GCH ∧ 𝒫 ℵ ⁡ A ∈ dom ⁡ card → ¬ ℵ ⁡ A ≺ ω
17 isfinite ⊢ ℵ ⁡ A ∈ Fin ↔ ℵ ⁡ A ≺ ω
18 16 17 sylnibr ⊢ A ∈ On ∧ ℵ ⁡ A ∈ GCH ∧ 𝒫 ℵ ⁡ A ∈ dom ⁡ card → ¬ ℵ ⁡ A ∈ Fin
19 simp2 ⊢ A ∈ On ∧ ℵ ⁡ A ∈ GCH ∧ 𝒫 ℵ ⁡ A ∈ dom ⁡ card → ℵ ⁡ A ∈ GCH
20 alephordilem1 ⊢ A ∈ On → ℵ ⁡ A ≺ ℵ ⁡ suc ⁡ A
21 20 3ad2ant1 ⊢ A ∈ On ∧ ℵ ⁡ A ∈ GCH ∧ 𝒫 ℵ ⁡ A ∈ dom ⁡ card → ℵ ⁡ A ≺ ℵ ⁡ suc ⁡ A
22 gchi ⊢ ℵ ⁡ A ∈ GCH ∧ ℵ ⁡ A ≺ ℵ ⁡ suc ⁡ A ∧ ℵ ⁡ suc ⁡ A ≺ 𝒫 ℵ ⁡ A → ℵ ⁡ A ∈ Fin
23 22 3expia ⊢ ℵ ⁡ A ∈ GCH ∧ ℵ ⁡ A ≺ ℵ ⁡ suc ⁡ A → ℵ ⁡ suc ⁡ A ≺ 𝒫 ℵ ⁡ A → ℵ ⁡ A ∈ Fin
24 19 21 23 syl2anc ⊢ A ∈ On ∧ ℵ ⁡ A ∈ GCH ∧ 𝒫 ℵ ⁡ A ∈ dom ⁡ card → ℵ ⁡ suc ⁡ A ≺ 𝒫 ℵ ⁡ A → ℵ ⁡ A ∈ Fin
25 18 24 mtod ⊢ A ∈ On ∧ ℵ ⁡ A ∈ GCH ∧ 𝒫 ℵ ⁡ A ∈ dom ⁡ card → ¬ ℵ ⁡ suc ⁡ A ≺ 𝒫 ℵ ⁡ A
26 domtri2 ⊢ 𝒫 ℵ ⁡ A ∈ dom ⁡ card ∧ ℵ ⁡ suc ⁡ A ∈ dom ⁡ card → 𝒫 ℵ ⁡ A ≼ ℵ ⁡ suc ⁡ A ↔ ¬ ℵ ⁡ suc ⁡ A ≺ 𝒫 ℵ ⁡ A
27 5 4 26 sylancl ⊢ A ∈ On ∧ ℵ ⁡ A ∈ GCH ∧ 𝒫 ℵ ⁡ A ∈ dom ⁡ card → 𝒫 ℵ ⁡ A ≼ ℵ ⁡ suc ⁡ A ↔ ¬ ℵ ⁡ suc ⁡ A ≺ 𝒫 ℵ ⁡ A
28 25 27 mpbird ⊢ A ∈ On ∧ ℵ ⁡ A ∈ GCH ∧ 𝒫 ℵ ⁡ A ∈ dom ⁡ card → 𝒫 ℵ ⁡ A ≼ ℵ ⁡ suc ⁡ A
29 sbth ⊢ ℵ ⁡ suc ⁡ A ≼ 𝒫 ℵ ⁡ A ∧ 𝒫 ℵ ⁡ A ≼ ℵ ⁡ suc ⁡ A → ℵ ⁡ suc ⁡ A ≈ 𝒫 ℵ ⁡ A
30 8 28 29 syl2anc ⊢ A ∈ On ∧ ℵ ⁡ A ∈ GCH ∧ 𝒫 ℵ ⁡ A ∈ dom ⁡ card → ℵ ⁡ suc ⁡ A ≈ 𝒫 ℵ ⁡ A