Metamath Proof Explorer

Theorem alephfp2

Description: The aleph function has at least one fixed point. Proposition 11.18 of TakeutiZaring p. 104. See alephfp for an actual example of a fixed point. Compare the inequality alephle that holds in general. Note that if x is a fixed point, then alephalephaleph` ... aleph `x = x . (Contributed by NM, 6-Nov-2004) (Revised by Mario Carneiro, 15-May-2015)

Ref Expression
Assertion alephfp2 ⊢ ∃ x ∈ On ℵ ⁡ x = x

Proof

Step Hyp Ref Expression
1 alephsson ⊢ ran ⁡ ℵ ⊆ On
2 eqid ⊢ rec ⁡ ℵ ω ↾ ω = rec ⁡ ℵ ω ↾ ω
3 2 alephfplem4 ⊢ ⋃ rec ⁡ ℵ ω ↾ ω ω ∈ ran ⁡ ℵ
4 1 3 sselii ⊢ ⋃ rec ⁡ ℵ ω ↾ ω ω ∈ On
5 2 alephfp ⊢ ℵ ⁡ ⋃ rec ⁡ ℵ ω ↾ ω ω = ⋃ rec ⁡ ℵ ω ↾ ω ω
6 fveq2 ⊢ x = ⋃ rec ⁡ ℵ ω ↾ ω ω → ℵ ⁡ x = ℵ ⁡ ⋃ rec ⁡ ℵ ω ↾ ω ω
7 id ⊢ x = ⋃ rec ⁡ ℵ ω ↾ ω ω → x = ⋃ rec ⁡ ℵ ω ↾ ω ω
8 6 7 eqeq12d ⊢ x = ⋃ rec ⁡ ℵ ω ↾ ω ω → ℵ ⁡ x = x ↔ ℵ ⁡ ⋃ rec ⁡ ℵ ω ↾ ω ω = ⋃ rec ⁡ ℵ ω ↾ ω ω
9 8 rspcev ⊢ ⋃ rec ⁡ ℵ ω ↾ ω ω ∈ On ∧ ℵ ⁡ ⋃ rec ⁡ ℵ ω ↾ ω ω = ⋃ rec ⁡ ℵ ω ↾ ω ω → ∃ x ∈ On ℵ ⁡ x = x
10 4 5 9 mp2an ⊢ ∃ x ∈ On ℵ ⁡ x = x