Metamath Proof Explorer

Theorem winafp

Description: A nontrivial weakly inaccessible cardinal is a fixed point of the aleph function. (Contributed by Mario Carneiro, 29-May-2014)

Ref Expression
Assertion winafp ( ( 𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω ) → ( ℵ ‘ 𝐴 ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 winalim2 ⊢ ( ( 𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω ) → ∃ 𝑥 ( ( ℵ ‘ 𝑥 ) = 𝐴 ∧ Lim 𝑥 ) )
2 vex ⊢ 𝑥 ∈ V
3 limelon ⊢ ( ( 𝑥 ∈ V ∧ Lim 𝑥 ) → 𝑥 ∈ On )
4 2 3 mpan ⊢ ( Lim 𝑥 → 𝑥 ∈ On )
5 alephle ⊢ ( 𝑥 ∈ On → 𝑥 ⊆ ( ℵ ‘ 𝑥 ) )
6 4 5 syl ⊢ ( Lim 𝑥 → 𝑥 ⊆ ( ℵ ‘ 𝑥 ) )
7 6 ad2antll ⊢ ( ( ( 𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω ) ∧ ( ( ℵ ‘ 𝑥 ) = 𝐴 ∧ Lim 𝑥 ) ) → 𝑥 ⊆ ( ℵ ‘ 𝑥 ) )
8 simprl ⊢ ( ( ( 𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω ) ∧ ( ( ℵ ‘ 𝑥 ) = 𝐴 ∧ Lim 𝑥 ) ) → ( ℵ ‘ 𝑥 ) = 𝐴 )
9 7 8 sseqtrd ⊢ ( ( ( 𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω ) ∧ ( ( ℵ ‘ 𝑥 ) = 𝐴 ∧ Lim 𝑥 ) ) → 𝑥 ⊆ 𝐴 )
10 8 fveq2d ⊢ ( ( ( 𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω ) ∧ ( ( ℵ ‘ 𝑥 ) = 𝐴 ∧ Lim 𝑥 ) ) → ( cf ‘ ( ℵ ‘ 𝑥 ) ) = ( cf ‘ 𝐴 ) )
11 alephsing ⊢ ( Lim 𝑥 → ( cf ‘ ( ℵ ‘ 𝑥 ) ) = ( cf ‘ 𝑥 ) )
12 11 ad2antll ⊢ ( ( ( 𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω ) ∧ ( ( ℵ ‘ 𝑥 ) = 𝐴 ∧ Lim 𝑥 ) ) → ( cf ‘ ( ℵ ‘ 𝑥 ) ) = ( cf ‘ 𝑥 ) )
13 10 12 eqtr3d ⊢ ( ( ( 𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω ) ∧ ( ( ℵ ‘ 𝑥 ) = 𝐴 ∧ Lim 𝑥 ) ) → ( cf ‘ 𝐴 ) = ( cf ‘ 𝑥 ) )
14 elwina ⊢ ( 𝐴 ∈ Inaccw ↔ ( 𝐴 ≠ ∅ ∧ ( cf ‘ 𝐴 ) = 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐴 𝑦 ≺ 𝑧 ) )
15 14 simp2bi ⊢ ( 𝐴 ∈ Inaccw → ( cf ‘ 𝐴 ) = 𝐴 )
16 15 ad2antrr ⊢ ( ( ( 𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω ) ∧ ( ( ℵ ‘ 𝑥 ) = 𝐴 ∧ Lim 𝑥 ) ) → ( cf ‘ 𝐴 ) = 𝐴 )
17 13 16 eqtr3d ⊢ ( ( ( 𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω ) ∧ ( ( ℵ ‘ 𝑥 ) = 𝐴 ∧ Lim 𝑥 ) ) → ( cf ‘ 𝑥 ) = 𝐴 )
18 cfle ⊢ ( cf ‘ 𝑥 ) ⊆ 𝑥
19 17 18 eqsstrrdi ⊢ ( ( ( 𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω ) ∧ ( ( ℵ ‘ 𝑥 ) = 𝐴 ∧ Lim 𝑥 ) ) → 𝐴 ⊆ 𝑥 )
20 9 19 eqssd ⊢ ( ( ( 𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω ) ∧ ( ( ℵ ‘ 𝑥 ) = 𝐴 ∧ Lim 𝑥 ) ) → 𝑥 = 𝐴 )
21 20 fveq2d ⊢ ( ( ( 𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω ) ∧ ( ( ℵ ‘ 𝑥 ) = 𝐴 ∧ Lim 𝑥 ) ) → ( ℵ ‘ 𝑥 ) = ( ℵ ‘ 𝐴 ) )
22 21 8 eqtr3d ⊢ ( ( ( 𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω ) ∧ ( ( ℵ ‘ 𝑥 ) = 𝐴 ∧ Lim 𝑥 ) ) → ( ℵ ‘ 𝐴 ) = 𝐴 )
23 1 22 exlimddv ⊢ ( ( 𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω ) → ( ℵ ‘ 𝐴 ) = 𝐴 )