This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 } )