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 ( ( 𝐴 ∈ On ∧ ( ℵ ‘ 𝐴 ) ∈ GCH ∧ 𝒫 ( ℵ ‘ 𝐴 ) ∈ dom card ) → ( ℵ ‘ suc 𝐴 ) ≈ 𝒫 ( ℵ ‘ 𝐴 ) )

Proof

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