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 ( 𝐹 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 ↾ 𝐴 ) ) )