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 ) = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) ≠ 𝑥 } )