Metamath Proof Explorer


Theorem fndmdif

Description: Two ways to express the locus of differences between two functions. (Contributed by Stefan O'Rear, 17-Jan-2015)

Ref Expression
Assertion fndmdif F Fn A G Fn A dom F G = x A | F x G x

Proof

Step Hyp Ref Expression
1 difss F G F
2 dmss F G F dom F G dom F
3 1 2 ax-mp dom F G dom F
4 fndm F Fn A dom F = A
5 4 adantr F Fn A G Fn A dom F = A
6 3 5 sseqtrid F Fn A G Fn A dom F G A
7 sseqin2 dom F G A A dom F G = dom F G
8 6 7 sylib F Fn A G Fn A A dom F G = dom F G
9 vex x V
10 9 eldm x dom F G y x F G y
11 eqcom F x = G x G x = F x
12 fnbrfvb G Fn A x A G x = F x x G F x
13 11 12 syl5bb G Fn A x A F x = G x x G F x
14 13 adantll F Fn A G Fn A x A F x = G x x G F x
15 14 necon3abid F Fn A G Fn A x A F x G x ¬ x G F x
16 fvex F x V
17 breq2 y = F x x G y x G F x
18 17 notbid y = F x ¬ x G y ¬ x G F x
19 16 18 ceqsexv y y = F x ¬ x G y ¬ x G F x
20 15 19 bitr4di F Fn A G Fn A x A F x G x y y = F x ¬ x G y
21 eqcom y = F x F x = y
22 fnbrfvb F Fn A x A F x = y x F y
23 21 22 syl5bb F Fn A x A y = F x x F y
24 23 adantlr F Fn A G Fn A x A y = F x x F y
25 24 anbi1d F Fn A G Fn A x A y = F x ¬ x G y x F y ¬ x G y
26 brdif x F G y x F y ¬ x G y
27 25 26 bitr4di F Fn A G Fn A x A y = F x ¬ x G y x F G y
28 27 exbidv F Fn A G Fn A x A y y = F x ¬ x G y y x F G y
29 20 28 bitr2d F Fn A G Fn A x A y x F G y F x G x
30 10 29 syl5bb F Fn A G Fn A x A x dom F G F x G x
31 30 rabbi2dva F Fn A G Fn A A dom F G = x A | F x G x
32 8 31 eqtr3d F Fn A G Fn A dom F G = x A | F x G x