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

Metamath Proof Explorer

Theorem fnnfpeq0

Description: A function is the identity iff it moves no points. (Contributed by Stefan O'Rear, 25-Aug-2015)

Ref Expression
Assertion fnnfpeq0 
|- ( F Fn A -> ( dom ( F \ _I ) = (/) <-> F = ( _I |` A ) ) )

Proof

Step Hyp Ref Expression
1 rabeq0 
 |-  ( { x e. A | ( F ` x ) =/= x } = (/) <-> A. x e. A -. ( F ` x ) =/= x )
2 nne 
 |-  ( -. ( F ` x ) =/= x <-> ( F ` x ) = x )
3 fvresi 
 |-  ( x e. A -> ( ( _I |` A ) ` x ) = x )
4 3 eqeq2d 
 |-  ( x e. A -> ( ( F ` x ) = ( ( _I |` A ) ` x ) <-> ( F ` x ) = x ) )
5 4 adantl 
 |-  ( ( F Fn A /\ x e. A ) -> ( ( F ` x ) = ( ( _I |` A ) ` x ) <-> ( F ` x ) = x ) )
6 2 5 bitr4id 
 |-  ( ( F Fn A /\ x e. A ) -> ( -. ( F ` x ) =/= x <-> ( F ` x ) = ( ( _I |` A ) ` x ) ) )
7 6 ralbidva 
 |-  ( F Fn A -> ( A. x e. A -. ( F ` x ) =/= x <-> A. x e. A ( F ` x ) = ( ( _I |` A ) ` x ) ) )
8 1 7 bitrid 
 |-  ( F Fn A -> ( { x e. A | ( F ` x ) =/= x } = (/) <-> A. x e. A ( F ` x ) = ( ( _I |` A ) ` x ) ) )
9 fndifnfp 
 |-  ( F Fn A -> dom ( F \ _I ) = { x e. A | ( F ` x ) =/= x } )
10 9 eqeq1d 
 |-  ( F Fn A -> ( dom ( F \ _I ) = (/) <-> { x e. A | ( F ` x ) =/= x } = (/) ) )
11 fnresi 
 |-  ( _I |` A ) Fn A
12 eqfnfv 
 |-  ( ( F Fn A /\ ( _I |` A ) Fn A ) -> ( F = ( _I |` A ) <-> A. x e. A ( F ` x ) = ( ( _I |` A ) ` x ) ) )
13 11 12 mpan2 
 |-  ( F Fn A -> ( F = ( _I |` A ) <-> A. x e. A ( F ` x ) = ( ( _I |` A ) ` x ) ) )
14 8 10 13 3bitr4d 
 |-  ( F Fn A -> ( dom ( F \ _I ) = (/) <-> F = ( _I |` A ) ) )