Theorem fnelfp

Description: Property of a fixed point of a function. (Contributed by Stefan O'Rear, 1-Feb-2015)

	Ref	Expression
Assertion	fnelfp	|- ( ( F Fn A /\ X e. A ) -> ( X e. dom ( F i^i _I ) <-> ( F ` X ) = X ) )

Proof

Step	Hyp	Ref	Expression
1		fninfp	|- ( F Fn A -> dom ( F i^i _I ) = { x e. A | ( F ` x ) = x } )
2	1	eleq2d	|- ( F Fn A -> ( X e. dom ( F i^i _I ) <-> X e. { x e. A | ( F ` x ) = x } ) )
3		fveq2	|- ( x = X -> ( F ` x ) = ( F ` X ) )
4		id	|- ( x = X -> x = X )
5	3 4	eqeq12d	|- ( x = X -> ( ( F ` x ) = x <-> ( F ` X ) = X ) )
6	5	elrab3	|- ( X e. A -> ( X e. { x e. A | ( F ` x ) = x } <-> ( F ` X ) = X ) )
7	2 6	sylan9bb	|- ( ( F Fn A /\ X e. A ) -> ( X e. dom ( F i^i _I ) <-> ( F ` X ) = X ) )