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