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	|- E. x e. On ( aleph ` x ) = x

Proof

Step	Hyp	Ref	Expression
1		alephsson	|- ran aleph C_ On
2		eqid	|- ( rec ( aleph , _om ) |` _om ) = ( rec ( aleph , _om ) |` _om )
3	2	alephfplem4	|- U. ( ( rec ( aleph , _om ) |` _om ) " _om ) e. ran aleph
4	1 3	sselii	|- U. ( ( rec ( aleph , _om ) |` _om ) " _om ) e. On
5	2	alephfp	|- ( aleph ` U. ( ( rec ( aleph , _om ) |` _om ) " _om ) ) = U. ( ( rec ( aleph , _om ) |` _om ) " _om )
6		fveq2	|- ( x = U. ( ( rec ( aleph , _om ) |` _om ) " _om ) -> ( aleph ` x ) = ( aleph ` U. ( ( rec ( aleph , _om ) |` _om ) " _om ) ) )
7		id	|- ( x = U. ( ( rec ( aleph , _om ) |` _om ) " _om ) -> x = U. ( ( rec ( aleph , _om ) |` _om ) " _om ) )
8	6 7	eqeq12d	|- ( x = U. ( ( rec ( aleph , _om ) |` _om ) " _om ) -> ( ( aleph ` x ) = x <-> ( aleph ` U. ( ( rec ( aleph , _om ) |` _om ) " _om ) ) = U. ( ( rec ( aleph , _om ) |` _om ) " _om ) ) )
9	8	rspcev	|- ( ( U. ( ( rec ( aleph , _om ) |` _om ) " _om ) e. On /\ ( aleph ` U. ( ( rec ( aleph , _om ) |` _om ) " _om ) ) = U. ( ( rec ( aleph , _om ) |` _om ) " _om ) ) -> E. x e. On ( aleph ` x ) = x )
10	4 5 9	mp2an	|- E. x e. On ( aleph ` x ) = x