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	$$⊢\exists x\in \mathrm{On}\aleph \left(x\right)=x$$

Proof

Step	Hyp	Ref	Expression
1		alephsson	$$⊢\mathrm{ran}\aleph \subseteq \mathrm{On}$$
2		eqid	$$⊢{\mathrm{rec}\left(\aleph ,\mathrm{\omega }\right)\upharpoonright }_{\mathrm{\omega }}={\mathrm{rec}\left(\aleph ,\mathrm{\omega }\right)\upharpoonright }_{\mathrm{\omega }}$$
3	2	alephfplem4	$$⊢\bigcup \left({\mathrm{rec}\left(\aleph ,\mathrm{\omega }\right)\upharpoonright }_{\mathrm{\omega }}\right)\left[\mathrm{\omega }\right]\in \mathrm{ran}\aleph$$
4	1 3	sselii	$$⊢\bigcup \left({\mathrm{rec}\left(\aleph ,\mathrm{\omega }\right)\upharpoonright }_{\mathrm{\omega }}\right)\left[\mathrm{\omega }\right]\in \mathrm{On}$$
5	2	alephfp	$$⊢\aleph \left(\bigcup \left({\mathrm{rec}\left(\aleph ,\mathrm{\omega }\right)\upharpoonright }_{\mathrm{\omega }}\right)\left[\mathrm{\omega }\right]\right)=\bigcup \left({\mathrm{rec}\left(\aleph ,\mathrm{\omega }\right)\upharpoonright }_{\mathrm{\omega }}\right)\left[\mathrm{\omega }\right]$$
6		fveq2	$$⊢x=\bigcup \left({\mathrm{rec}\left(\aleph ,\mathrm{\omega }\right)\upharpoonright }_{\mathrm{\omega }}\right)\left[\mathrm{\omega }\right]\to \aleph \left(x\right)=\aleph \left(\bigcup \left({\mathrm{rec}\left(\aleph ,\mathrm{\omega }\right)\upharpoonright }_{\mathrm{\omega }}\right)\left[\mathrm{\omega }\right]\right)$$
7		id	$$⊢x=\bigcup \left({\mathrm{rec}\left(\aleph ,\mathrm{\omega }\right)\upharpoonright }_{\mathrm{\omega }}\right)\left[\mathrm{\omega }\right]\to x=\bigcup \left({\mathrm{rec}\left(\aleph ,\mathrm{\omega }\right)\upharpoonright }_{\mathrm{\omega }}\right)\left[\mathrm{\omega }\right]$$
8	6 7	eqeq12d	$$⊢x=\bigcup \left({\mathrm{rec}\left(\aleph ,\mathrm{\omega }\right)\upharpoonright }_{\mathrm{\omega }}\right)\left[\mathrm{\omega }\right]\to \left(\aleph \left(x\right)=x\leftrightarrow \aleph \left(\bigcup \left({\mathrm{rec}\left(\aleph ,\mathrm{\omega }\right)\upharpoonright }_{\mathrm{\omega }}\right)\left[\mathrm{\omega }\right]\right)=\bigcup \left({\mathrm{rec}\left(\aleph ,\mathrm{\omega }\right)\upharpoonright }_{\mathrm{\omega }}\right)\left[\mathrm{\omega }\right]\right)$$
9	8	rspcev	$$⊢\left(\bigcup \left({\mathrm{rec}\left(\aleph ,\mathrm{\omega }\right)\upharpoonright }_{\mathrm{\omega }}\right)\left[\mathrm{\omega }\right]\in \mathrm{On}\wedge \aleph \left(\bigcup \left({\mathrm{rec}\left(\aleph ,\mathrm{\omega }\right)\upharpoonright }_{\mathrm{\omega }}\right)\left[\mathrm{\omega }\right]\right)=\bigcup \left({\mathrm{rec}\left(\aleph ,\mathrm{\omega }\right)\upharpoonright }_{\mathrm{\omega }}\right)\left[\mathrm{\omega }\right]\right)\to \exists x\in \mathrm{On}\aleph \left(x\right)=x$$
10	4 5 9	mp2an	$$⊢\exists x\in \mathrm{On}\aleph \left(x\right)=x$$