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 ) } )