Theorem fninfp

Description: Express the class of fixed points of a function. (Contributed by Stefan O'Rear, 1-Feb-2015)

	Ref	Expression
Assertion	fninfp	|- ( F Fn A -> dom ( F i^i _I ) = { x e. A | ( F ` x ) = x } )

Proof

Step	Hyp	Ref	Expression
1		inres	|- ( _I i^i ( F |` A ) ) = ( ( _I i^i F ) |` A )
2		incom	|- ( _I i^i F ) = ( F i^i _I )
3	2	reseq1i	|- ( ( _I i^i F ) |` A ) = ( ( F i^i _I ) |` A )
4	1 3	eqtri	|- ( _I i^i ( F |` A ) ) = ( ( F i^i _I ) |` A )
5		incom	|- ( ( F |` A ) i^i _I ) = ( _I i^i ( F |` A ) )
6		inres	|- ( F i^i ( _I |` A ) ) = ( ( F i^i _I ) |` A )
7	4 5 6	3eqtr4i	|- ( ( F |` A ) i^i _I ) = ( F i^i ( _I |` A ) )
8		fnresdm	|- ( F Fn A -> ( F |` A ) = F )
9	8	ineq1d	|- ( F Fn A -> ( ( F |` A ) i^i _I ) = ( F i^i _I ) )
10	7 9	syl5reqr	|- ( F Fn A -> ( F i^i _I ) = ( F i^i ( _I |` A ) ) )
11	10	dmeqd	|- ( F Fn A -> dom ( F i^i _I ) = dom ( F i^i ( _I |` A ) ) )
12		fnresi	|- ( _I |` A ) Fn A
13		fndmin	|- ( ( F Fn A /\ ( _I |` A ) Fn A ) -> dom ( F i^i ( _I |` A ) ) = { x e. A | ( F ` x ) = ( ( _I |` A ) ` x ) } )
14	12 13	mpan2	|- ( F Fn A -> dom ( F i^i ( _I |` A ) ) = { x e. A | ( F ` x ) = ( ( _I |` A ) ` x ) } )
15		fvresi	|- ( x e. A -> ( ( _I |` A ) ` x ) = x )
16	15	eqeq2d	|- ( x e. A -> ( ( F ` x ) = ( ( _I |` A ) ` x ) <-> ( F ` x ) = x ) )
17	16	rabbiia	|- { x e. A | ( F ` x ) = ( ( _I |` A ) ` x ) } = { x e. A | ( F ` x ) = x }
18	17	a1i	|- ( F Fn A -> { x e. A | ( F ` x ) = ( ( _I |` A ) ` x ) } = { x e. A | ( F ` x ) = x } )
19	11 14 18	3eqtrd	|- ( F Fn A -> dom ( F i^i _I ) = { x e. A | ( F ` x ) = x } )