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	⊢ ∃ 𝑥 ∈ On ( ℵ ‘ 𝑥 ) = 𝑥

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	⊢ ( 𝑥 = ∪ ( ( rec ( ℵ , ω ) ↾ ω ) “ ω ) → ( ℵ ‘ 𝑥 ) = ( ℵ ‘ ∪ ( ( rec ( ℵ , ω ) ↾ ω ) “ ω ) ) )
7		id	⊢ ( 𝑥 = ∪ ( ( rec ( ℵ , ω ) ↾ ω ) “ ω ) → 𝑥 = ∪ ( ( rec ( ℵ , ω ) ↾ ω ) “ ω ) )
8	6 7	eqeq12d	⊢ ( 𝑥 = ∪ ( ( rec ( ℵ , ω ) ↾ ω ) “ ω ) → ( ( ℵ ‘ 𝑥 ) = 𝑥 ↔ ( ℵ ‘ ∪ ( ( rec ( ℵ , ω ) ↾ ω ) “ ω ) ) = ∪ ( ( rec ( ℵ , ω ) ↾ ω ) “ ω ) ) )
9	8	rspcev	⊢ ( ( ∪ ( ( rec ( ℵ , ω ) ↾ ω ) “ ω ) ∈ On ∧ ( ℵ ‘ ∪ ( ( rec ( ℵ , ω ) ↾ ω ) “ ω ) ) = ∪ ( ( rec ( ℵ , ω ) ↾ ω ) “ ω ) ) → ∃ 𝑥 ∈ On ( ℵ ‘ 𝑥 ) = 𝑥 )
10	4 5 9	mp2an	⊢ ∃ 𝑥 ∈ On ( ℵ ‘ 𝑥 ) = 𝑥