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	⊢ ( 𝐹 Fn 𝐴 → ( dom ( 𝐹 ∖ I ) = ∅ ↔ 𝐹 = ( I ↾ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rabeq0	⊢ ( { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) ≠ 𝑥 } = ∅ ↔ ∀ 𝑥 ∈ 𝐴 ¬ ( 𝐹 ‘ 𝑥 ) ≠ 𝑥 )
2		nne	⊢ ( ¬ ( 𝐹 ‘ 𝑥 ) ≠ 𝑥 ↔ ( 𝐹 ‘ 𝑥 ) = 𝑥 )
3		fvresi	⊢ ( 𝑥 ∈ 𝐴 → ( ( I ↾ 𝐴 ) ‘ 𝑥 ) = 𝑥 )
4	3	eqeq2d	⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝐹 ‘ 𝑥 ) = ( ( I ↾ 𝐴 ) ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑥 ) = 𝑥 ) )
5	4	adantl	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) = ( ( I ↾ 𝐴 ) ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑥 ) = 𝑥 ) )
6	2 5	bitr4id	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ¬ ( 𝐹 ‘ 𝑥 ) ≠ 𝑥 ↔ ( 𝐹 ‘ 𝑥 ) = ( ( I ↾ 𝐴 ) ‘ 𝑥 ) ) )
7	6	ralbidva	⊢ ( 𝐹 Fn 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ¬ ( 𝐹 ‘ 𝑥 ) ≠ 𝑥 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( ( I ↾ 𝐴 ) ‘ 𝑥 ) ) )
8	1 7	syl5bb	⊢ ( 𝐹 Fn 𝐴 → ( { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) ≠ 𝑥 } = ∅ ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( ( I ↾ 𝐴 ) ‘ 𝑥 ) ) )
9		fndifnfp	⊢ ( 𝐹 Fn 𝐴 → dom ( 𝐹 ∖ I ) = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) ≠ 𝑥 } )
10	9	eqeq1d	⊢ ( 𝐹 Fn 𝐴 → ( dom ( 𝐹 ∖ I ) = ∅ ↔ { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) ≠ 𝑥 } = ∅ ) )
11		fnresi	⊢ ( I ↾ 𝐴 ) Fn 𝐴
12		eqfnfv	⊢ ( ( 𝐹 Fn 𝐴 ∧ ( I ↾ 𝐴 ) Fn 𝐴 ) → ( 𝐹 = ( I ↾ 𝐴 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( ( I ↾ 𝐴 ) ‘ 𝑥 ) ) )
13	11 12	mpan2	⊢ ( 𝐹 Fn 𝐴 → ( 𝐹 = ( I ↾ 𝐴 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( ( I ↾ 𝐴 ) ‘ 𝑥 ) ) )
14	8 10 13	3bitr4d	⊢ ( 𝐹 Fn 𝐴 → ( dom ( 𝐹 ∖ I ) = ∅ ↔ 𝐹 = ( I ↾ 𝐴 ) ) )