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 F Fn A dom F I = x A | F x x

Proof

Step Hyp Ref Expression
1 dffn2 F Fn A F : A V
2 fssxp F : A V F A × V
3 1 2 sylbi F Fn A F A × V
4 ssdif0 F A × V F A × V =
5 3 4 sylib F Fn A F A × V =
6 5 uneq2d F Fn A F I F A × V = F I
7 un0 F I = F I
8 6 7 eqtr2di F Fn A F I = F I F A × V
9 df-res I A = I A × V
10 9 difeq2i F I A = F I A × V
11 difindi F I A × V = F I F A × V
12 10 11 eqtri F I A = F I F A × V
13 8 12 eqtr4di F Fn A F I = F I A
14 13 dmeqd F Fn A dom F I = dom F I A
15 fnresi I A Fn A
16 fndmdif F Fn A I A Fn A dom F I A = x A | F x I A x
17 15 16 mpan2 F Fn A dom F I A = x A | F x I A x
18 fvresi x A I A x = x
19 18 neeq2d x A F x I A x F x x
20 19 rabbiia x A | F x I A x = x A | F x x
21 20 a1i F Fn A x A | F x I A x = x A | F x x
22 14 17 21 3eqtrd F Fn A dom F I = x A | F x x