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 e. A | ( F ` x ) =/= ( G ` x ) } )

Proof

Step Hyp Ref Expression
1 difss
 |-  ( F \ G ) C_ F
2 dmss
 |-  ( ( F \ G ) C_ F -> dom ( F \ G ) C_ dom F )
3 1 2 ax-mp
 |-  dom ( F \ G ) C_ 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 ) C_ A )
7 sseqin2
 |-  ( dom ( F \ G ) C_ A <-> ( A i^i dom ( F \ G ) ) = dom ( F \ G ) )
8 6 7 sylib
 |-  ( ( F Fn A /\ G Fn A ) -> ( A i^i dom ( F \ G ) ) = dom ( F \ G ) )
9 vex
 |-  x e. _V
10 9 eldm
 |-  ( x e. dom ( F \ G ) <-> E. y x ( F \ G ) y )
11 eqcom
 |-  ( ( F ` x ) = ( G ` x ) <-> ( G ` x ) = ( F ` x ) )
12 fnbrfvb
 |-  ( ( G Fn A /\ x e. A ) -> ( ( G ` x ) = ( F ` x ) <-> x G ( F ` x ) ) )
13 11 12 syl5bb
 |-  ( ( G Fn A /\ x e. A ) -> ( ( F ` x ) = ( G ` x ) <-> x G ( F ` x ) ) )
14 13 adantll
 |-  ( ( ( F Fn A /\ G Fn A ) /\ x e. A ) -> ( ( F ` x ) = ( G ` x ) <-> x G ( F ` x ) ) )
15 14 necon3abid
 |-  ( ( ( F Fn A /\ G Fn A ) /\ x e. A ) -> ( ( F ` x ) =/= ( G ` x ) <-> -. x G ( F ` x ) ) )
16 fvex
 |-  ( F ` x ) e. _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
 |-  ( E. y ( y = ( F ` x ) /\ -. x G y ) <-> -. x G ( F ` x ) )
20 15 19 bitr4di
 |-  ( ( ( F Fn A /\ G Fn A ) /\ x e. A ) -> ( ( F ` x ) =/= ( G ` x ) <-> E. y ( y = ( F ` x ) /\ -. x G y ) ) )
21 eqcom
 |-  ( y = ( F ` x ) <-> ( F ` x ) = y )
22 fnbrfvb
 |-  ( ( F Fn A /\ x e. A ) -> ( ( F ` x ) = y <-> x F y ) )
23 21 22 syl5bb
 |-  ( ( F Fn A /\ x e. A ) -> ( y = ( F ` x ) <-> x F y ) )
24 23 adantlr
 |-  ( ( ( F Fn A /\ G Fn A ) /\ x e. A ) -> ( y = ( F ` x ) <-> x F y ) )
25 24 anbi1d
 |-  ( ( ( F Fn A /\ G Fn A ) /\ x e. 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 e. A ) -> ( ( y = ( F ` x ) /\ -. x G y ) <-> x ( F \ G ) y ) )
28 27 exbidv
 |-  ( ( ( F Fn A /\ G Fn A ) /\ x e. A ) -> ( E. y ( y = ( F ` x ) /\ -. x G y ) <-> E. y x ( F \ G ) y ) )
29 20 28 bitr2d
 |-  ( ( ( F Fn A /\ G Fn A ) /\ x e. A ) -> ( E. y x ( F \ G ) y <-> ( F ` x ) =/= ( G ` x ) ) )
30 10 29 syl5bb
 |-  ( ( ( F Fn A /\ G Fn A ) /\ x e. A ) -> ( x e. dom ( F \ G ) <-> ( F ` x ) =/= ( G ` x ) ) )
31 30 rabbi2dva
 |-  ( ( F Fn A /\ G Fn A ) -> ( A i^i dom ( F \ G ) ) = { x e. A | ( F ` x ) =/= ( G ` x ) } )
32 8 31 eqtr3d
 |-  ( ( F Fn A /\ G Fn A ) -> dom ( F \ G ) = { x e. A | ( F ` x ) =/= ( G ` x ) } )