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

Metamath Proof Explorer

Theorem fndifnfp

Description: Express the class of non-fixed points of a function. (Contributed by Stefan O'Rear, 14-Aug-2015)

Ref Expression
Assertion fndifnfp ( 𝐹 Fn 𝐴 → dom ( 𝐹 ∖ I ) = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) ≠ 𝑥 } )

Proof

Step Hyp Ref Expression
1 dffn2 ⊢ ( 𝐹 Fn 𝐴 ↔ 𝐹 : 𝐴 ⟶ V )
2 fssxp ⊢ ( 𝐹 : 𝐴 ⟶ V → 𝐹 ⊆ ( 𝐴 × V ) )
3 1 2 sylbi ⊢ ( 𝐹 Fn 𝐴 → 𝐹 ⊆ ( 𝐴 × V ) )
4 ssdif0 ⊢ ( 𝐹 ⊆ ( 𝐴 × V ) ↔ ( 𝐹 ∖ ( 𝐴 × V ) ) = ∅ )
5 3 4 sylib ⊢ ( 𝐹 Fn 𝐴 → ( 𝐹 ∖ ( 𝐴 × V ) ) = ∅ )
6 5 uneq2d ⊢ ( 𝐹 Fn 𝐴 → ( ( 𝐹 ∖ I ) ∪ ( 𝐹 ∖ ( 𝐴 × V ) ) ) = ( ( 𝐹 ∖ I ) ∪ ∅ ) )
7 un0 ⊢ ( ( 𝐹 ∖ I ) ∪ ∅ ) = ( 𝐹 ∖ I )
8 6 7 eqtr2di ⊢ ( 𝐹 Fn 𝐴 → ( 𝐹 ∖ I ) = ( ( 𝐹 ∖ I ) ∪ ( 𝐹 ∖ ( 𝐴 × V ) ) ) )
9 df-res ⊢ ( I ↾ 𝐴 ) = ( I ∩ ( 𝐴 × V ) )
10 9 difeq2i ⊢ ( 𝐹 ∖ ( I ↾ 𝐴 ) ) = ( 𝐹 ∖ ( I ∩ ( 𝐴 × V ) ) )
11 difindi ⊢ ( 𝐹 ∖ ( I ∩ ( 𝐴 × V ) ) ) = ( ( 𝐹 ∖ I ) ∪ ( 𝐹 ∖ ( 𝐴 × V ) ) )
12 10 11 eqtri ⊢ ( 𝐹 ∖ ( I ↾ 𝐴 ) ) = ( ( 𝐹 ∖ I ) ∪ ( 𝐹 ∖ ( 𝐴 × V ) ) )
13 8 12 eqtr4di ⊢ ( 𝐹 Fn 𝐴 → ( 𝐹 ∖ I ) = ( 𝐹 ∖ ( I ↾ 𝐴 ) ) )
14 13 dmeqd ⊢ ( 𝐹 Fn 𝐴 → dom ( 𝐹 ∖ I ) = dom ( 𝐹 ∖ ( I ↾ 𝐴 ) ) )
15 fnresi ⊢ ( I ↾ 𝐴 ) Fn 𝐴
16 fndmdif ⊢ ( ( 𝐹 Fn 𝐴 ∧ ( I ↾ 𝐴 ) Fn 𝐴 ) → dom ( 𝐹 ∖ ( I ↾ 𝐴 ) ) = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) ≠ ( ( I ↾ 𝐴 ) ‘ 𝑥 ) } )
17 15 16 mpan2 ⊢ ( 𝐹 Fn 𝐴 → dom ( 𝐹 ∖ ( I ↾ 𝐴 ) ) = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) ≠ ( ( I ↾ 𝐴 ) ‘ 𝑥 ) } )
18 fvresi ⊢ ( 𝑥 ∈ 𝐴 → ( ( I ↾ 𝐴 ) ‘ 𝑥 ) = 𝑥 )
19 18 neeq2d ⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝐹 ‘ 𝑥 ) ≠ ( ( I ↾ 𝐴 ) ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑥 ) ≠ 𝑥 ) )
20 19 rabbiia ⊢ { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) ≠ ( ( I ↾ 𝐴 ) ‘ 𝑥 ) } = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) ≠ 𝑥 }
21 20 a1i ⊢ ( 𝐹 Fn 𝐴 → { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) ≠ ( ( I ↾ 𝐴 ) ‘ 𝑥 ) } = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) ≠ 𝑥 } )
22 14 17 21 3eqtrd ⊢ ( 𝐹 Fn 𝐴 → dom ( 𝐹 ∖ I ) = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) ≠ 𝑥 } )