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	syl5bb	|- ( 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 ) ) )