Theorem fndifnfp

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

	Ref	Expression
Assertion	fndifnfp	|- ( F Fn A -> dom ( F \ _I ) = { x e. A | ( F ` x ) =/= x } )

Proof

Step	Hyp	Ref	Expression
1		dffn2	|- ( F Fn A <-> F : A --> _V )
2		fssxp	|- ( F : A --> _V -> F C_ ( A X. _V ) )
3	1 2	sylbi	|- ( F Fn A -> F C_ ( A X. _V ) )
4		ssdif0	|- ( F C_ ( A X. _V ) <-> ( F \ ( A X. _V ) ) = (/) )
5	3 4	sylib	|- ( F Fn A -> ( F \ ( A X. _V ) ) = (/) )
6	5	uneq2d	|- ( F Fn A -> ( ( F \ _I ) u. ( F \ ( A X. _V ) ) ) = ( ( F \ _I ) u. (/) ) )
7		un0	|- ( ( F \ _I ) u. (/) ) = ( F \ _I )
8	6 7	eqtr2di	|- ( F Fn A -> ( F \ _I ) = ( ( F \ _I ) u. ( F \ ( A X. _V ) ) ) )
9		df-res	|- ( _I |` A ) = ( _I i^i ( A X. _V ) )
10	9	difeq2i	|- ( F \ ( _I |` A ) ) = ( F \ ( _I i^i ( A X. _V ) ) )
11		difindi	|- ( F \ ( _I i^i ( A X. _V ) ) ) = ( ( F \ _I ) u. ( F \ ( A X. _V ) ) )
12	10 11	eqtri	|- ( F \ ( _I |` A ) ) = ( ( F \ _I ) u. ( F \ ( A X. _V ) ) )
13	8 12	eqtr4di	|- ( F Fn A -> ( F \ _I ) = ( F \ ( _I |` A ) ) )
14	13	dmeqd	|- ( F Fn A -> dom ( F \ _I ) = dom ( F \ ( _I |` A ) ) )
15		fnresi	|- ( _I |` A ) Fn A
16		fndmdif	|- ( ( F Fn A /\ ( _I |` A ) Fn A ) -> dom ( F \ ( _I |` A ) ) = { x e. A | ( F ` x ) =/= ( ( _I |` A ) ` x ) } )
17	15 16	mpan2	|- ( F Fn A -> dom ( F \ ( _I |` A ) ) = { x e. A | ( F ` x ) =/= ( ( _I |` A ) ` x ) } )
18		fvresi	|- ( x e. A -> ( ( _I |` A ) ` x ) = x )
19	18	neeq2d	|- ( x e. A -> ( ( F ` x ) =/= ( ( _I |` A ) ` x ) <-> ( F ` x ) =/= x ) )
20	19	rabbiia	|- { x e. A | ( F ` x ) =/= ( ( _I |` A ) ` x ) } = { x e. A | ( F ` x ) =/= x }
21	20	a1i	|- ( F Fn A -> { x e. A | ( F ` x ) =/= ( ( _I |` A ) ` x ) } = { x e. A | ( F ` x ) =/= x } )
22	14 17 21	3eqtrd	|- ( F Fn A -> dom ( F \ _I ) = { x e. A | ( F ` x ) =/= x } )