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 ∈ A | F ⁡ x ≠ x = ∅ ↔ ∀ x ∈ A ¬ F ⁡ x ≠ x
2 nne ⊢ ¬ F ⁡ x ≠ x ↔ F ⁡ x = x
3 fvresi ⊢ x ∈ A → I ↾ A ⁡ x = x
4 3 eqeq2d ⊢ x ∈ A → F ⁡ x = I ↾ A ⁡ x ↔ F ⁡ x = x
5 4 adantl ⊢ F Fn A ∧ x ∈ A → F ⁡ x = I ↾ A ⁡ x ↔ F ⁡ x = x
6 2 5 bitr4id ⊢ F Fn A ∧ x ∈ A → ¬ F ⁡ x ≠ x ↔ F ⁡ x = I ↾ A ⁡ x
7 6 ralbidva ⊢ F Fn A → ∀ x ∈ A ¬ F ⁡ x ≠ x ↔ ∀ x ∈ A F ⁡ x = I ↾ A ⁡ x
8 1 7 bitrid ⊢ F Fn A → x ∈ A | F ⁡ x ≠ x = ∅ ↔ ∀ x ∈ A F ⁡ x = I ↾ A ⁡ x
9 fndifnfp ⊢ F Fn A → dom ⁡ F ∖ I = x ∈ A | F ⁡ x ≠ x
10 9 eqeq1d ⊢ F Fn A → dom ⁡ F ∖ I = ∅ ↔ x ∈ A | F ⁡ x ≠ x = ∅
11 fnresi ⊢ I ↾ A Fn A
12 eqfnfv ⊢ F Fn A ∧ I ↾ A Fn A → F = I ↾ A ↔ ∀ x ∈ A F ⁡ x = I ↾ A ⁡ x
13 11 12 mpan2 ⊢ F Fn A → F = I ↾ A ↔ ∀ x ∈ A F ⁡ x = I ↾ A ⁡ x
14 8 10 13 3bitr4d ⊢ F Fn A → dom ⁡ F ∖ I = ∅ ↔ F = I ↾ A