MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imadif Structured version   Unicode version

Theorem imadif 5661
Description: The image of a difference is the difference of images. (Contributed by NM, 24-May-1998.)
Assertion
Ref Expression
imadif  |-  ( Fun  `' F  ->  ( F
" ( A  \  B ) )  =  ( ( F " A )  \  ( F " B ) ) )

Proof of Theorem imadif
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 anandir 827 . . . . . . . 8  |-  ( ( ( x  e.  A  /\  -.  x  e.  B
)  /\  x F
y )  <->  ( (
x  e.  A  /\  x F y )  /\  ( -.  x  e.  B  /\  x F y ) ) )
21exbii 1644 . . . . . . 7  |-  ( E. x ( ( x  e.  A  /\  -.  x  e.  B )  /\  x F y )  <->  E. x ( ( x  e.  A  /\  x F y )  /\  ( -.  x  e.  B  /\  x F y ) ) )
3 19.40 1656 . . . . . . 7  |-  ( E. x ( ( x  e.  A  /\  x F y )  /\  ( -.  x  e.  B  /\  x F y ) )  ->  ( E. x ( x  e.  A  /\  x F y )  /\  E. x ( -.  x  e.  B  /\  x F y ) ) )
42, 3sylbi 195 . . . . . 6  |-  ( E. x ( ( x  e.  A  /\  -.  x  e.  B )  /\  x F y )  ->  ( E. x
( x  e.  A  /\  x F y )  /\  E. x ( -.  x  e.  B  /\  x F y ) ) )
5 nfv 1683 . . . . . . . . . . 11  |-  F/ x Fun  `' F
6 nfe1 1789 . . . . . . . . . . 11  |-  F/ x E. x ( x F y  /\  -.  x  e.  B )
75, 6nfan 1875 . . . . . . . . . 10  |-  F/ x
( Fun  `' F  /\  E. x ( x F y  /\  -.  x  e.  B )
)
8 funmo 5602 . . . . . . . . . . . . . 14  |-  ( Fun  `' F  ->  E* x  y `' F x )
9 vex 3116 . . . . . . . . . . . . . . . 16  |-  y  e. 
_V
10 vex 3116 . . . . . . . . . . . . . . . 16  |-  x  e. 
_V
119, 10brcnv 5183 . . . . . . . . . . . . . . 15  |-  ( y `' F x  <->  x F
y )
1211mobii 2301 . . . . . . . . . . . . . 14  |-  ( E* x  y `' F x 
<->  E* x  x F y )
138, 12sylib 196 . . . . . . . . . . . . 13  |-  ( Fun  `' F  ->  E* x  x F y )
14 mopick 2361 . . . . . . . . . . . . 13  |-  ( ( E* x  x F y  /\  E. x
( x F y  /\  -.  x  e.  B ) )  -> 
( x F y  ->  -.  x  e.  B ) )
1513, 14sylan 471 . . . . . . . . . . . 12  |-  ( ( Fun  `' F  /\  E. x ( x F y  /\  -.  x  e.  B ) )  -> 
( x F y  ->  -.  x  e.  B ) )
1615con2d 115 . . . . . . . . . . 11  |-  ( ( Fun  `' F  /\  E. x ( x F y  /\  -.  x  e.  B ) )  -> 
( x  e.  B  ->  -.  x F y ) )
17 imnan 422 . . . . . . . . . . 11  |-  ( ( x  e.  B  ->  -.  x F y )  <->  -.  ( x  e.  B  /\  x F y ) )
1816, 17sylib 196 . . . . . . . . . 10  |-  ( ( Fun  `' F  /\  E. x ( x F y  /\  -.  x  e.  B ) )  ->  -.  ( x  e.  B  /\  x F y ) )
197, 18alrimi 1825 . . . . . . . . 9  |-  ( ( Fun  `' F  /\  E. x ( x F y  /\  -.  x  e.  B ) )  ->  A. x  -.  (
x  e.  B  /\  x F y ) )
2019ex 434 . . . . . . . 8  |-  ( Fun  `' F  ->  ( E. x ( x F y  /\  -.  x  e.  B )  ->  A. x  -.  ( x  e.  B  /\  x F y ) ) )
21 exancom 1648 . . . . . . . 8  |-  ( E. x ( x F y  /\  -.  x  e.  B )  <->  E. x
( -.  x  e.  B  /\  x F y ) )
22 alnex 1598 . . . . . . . 8  |-  ( A. x  -.  ( x  e.  B  /\  x F y )  <->  -.  E. x
( x  e.  B  /\  x F y ) )
2320, 21, 223imtr3g 269 . . . . . . 7  |-  ( Fun  `' F  ->  ( E. x ( -.  x  e.  B  /\  x F y )  ->  -.  E. x ( x  e.  B  /\  x F y ) ) )
2423anim2d 565 . . . . . 6  |-  ( Fun  `' F  ->  ( ( E. x ( x  e.  A  /\  x F y )  /\  E. x ( -.  x  e.  B  /\  x F y ) )  ->  ( E. x
( x  e.  A  /\  x F y )  /\  -.  E. x
( x  e.  B  /\  x F y ) ) ) )
254, 24syl5 32 . . . . 5  |-  ( Fun  `' F  ->  ( E. x ( ( x  e.  A  /\  -.  x  e.  B )  /\  x F y )  ->  ( E. x
( x  e.  A  /\  x F y )  /\  -.  E. x
( x  e.  B  /\  x F y ) ) ) )
26 19.29r 1661 . . . . . . 7  |-  ( ( E. x ( x  e.  A  /\  x F y )  /\  A. x  -.  ( x  e.  B  /\  x F y ) )  ->  E. x ( ( x  e.  A  /\  x F y )  /\  -.  ( x  e.  B  /\  x F y ) ) )
2722, 26sylan2br 476 . . . . . 6  |-  ( ( E. x ( x  e.  A  /\  x F y )  /\  -.  E. x ( x  e.  B  /\  x F y ) )  ->  E. x ( ( x  e.  A  /\  x F y )  /\  -.  ( x  e.  B  /\  x F y ) ) )
28 andi 865 . . . . . . . 8  |-  ( ( ( x  e.  A  /\  x F y )  /\  ( -.  x  e.  B  \/  -.  x F y ) )  <-> 
( ( ( x  e.  A  /\  x F y )  /\  -.  x  e.  B
)  \/  ( ( x  e.  A  /\  x F y )  /\  -.  x F y ) ) )
29 ianor 488 . . . . . . . . 9  |-  ( -.  ( x  e.  B  /\  x F y )  <-> 
( -.  x  e.  B  \/  -.  x F y ) )
3029anbi2i 694 . . . . . . . 8  |-  ( ( ( x  e.  A  /\  x F y )  /\  -.  ( x  e.  B  /\  x F y ) )  <-> 
( ( x  e.  A  /\  x F y )  /\  ( -.  x  e.  B  \/  -.  x F y ) ) )
31 an32 796 . . . . . . . . 9  |-  ( ( ( x  e.  A  /\  -.  x  e.  B
)  /\  x F
y )  <->  ( (
x  e.  A  /\  x F y )  /\  -.  x  e.  B
) )
32 pm3.24 880 . . . . . . . . . . . 12  |-  -.  (
x F y  /\  -.  x F y )
3332intnan 912 . . . . . . . . . . 11  |-  -.  (
x  e.  A  /\  ( x F y  /\  -.  x F y ) )
34 anass 649 . . . . . . . . . . 11  |-  ( ( ( x  e.  A  /\  x F y )  /\  -.  x F y )  <->  ( x  e.  A  /\  (
x F y  /\  -.  x F y ) ) )
3533, 34mtbir 299 . . . . . . . . . 10  |-  -.  (
( x  e.  A  /\  x F y )  /\  -.  x F y )
3635biorfi 407 . . . . . . . . 9  |-  ( ( ( x  e.  A  /\  x F y )  /\  -.  x  e.  B )  <->  ( (
( x  e.  A  /\  x F y )  /\  -.  x  e.  B )  \/  (
( x  e.  A  /\  x F y )  /\  -.  x F y ) ) )
3731, 36bitri 249 . . . . . . . 8  |-  ( ( ( x  e.  A  /\  -.  x  e.  B
)  /\  x F
y )  <->  ( (
( x  e.  A  /\  x F y )  /\  -.  x  e.  B )  \/  (
( x  e.  A  /\  x F y )  /\  -.  x F y ) ) )
3828, 30, 373bitr4i 277 . . . . . . 7  |-  ( ( ( x  e.  A  /\  x F y )  /\  -.  ( x  e.  B  /\  x F y ) )  <-> 
( ( x  e.  A  /\  -.  x  e.  B )  /\  x F y ) )
3938exbii 1644 . . . . . 6  |-  ( E. x ( ( x  e.  A  /\  x F y )  /\  -.  ( x  e.  B  /\  x F y ) )  <->  E. x ( ( x  e.  A  /\  -.  x  e.  B
)  /\  x F
y ) )
4027, 39sylib 196 . . . . 5  |-  ( ( E. x ( x  e.  A  /\  x F y )  /\  -.  E. x ( x  e.  B  /\  x F y ) )  ->  E. x ( ( x  e.  A  /\  -.  x  e.  B
)  /\  x F
y ) )
4125, 40impbid1 203 . . . 4  |-  ( Fun  `' F  ->  ( E. x ( ( x  e.  A  /\  -.  x  e.  B )  /\  x F y )  <-> 
( E. x ( x  e.  A  /\  x F y )  /\  -.  E. x ( x  e.  B  /\  x F y ) ) ) )
42 eldif 3486 . . . . . 6  |-  ( x  e.  ( A  \  B )  <->  ( x  e.  A  /\  -.  x  e.  B ) )
4342anbi1i 695 . . . . 5  |-  ( ( x  e.  ( A 
\  B )  /\  x F y )  <->  ( (
x  e.  A  /\  -.  x  e.  B
)  /\  x F
y ) )
4443exbii 1644 . . . 4  |-  ( E. x ( x  e.  ( A  \  B
)  /\  x F
y )  <->  E. x
( ( x  e.  A  /\  -.  x  e.  B )  /\  x F y ) )
459elima2 5341 . . . . 5  |-  ( y  e.  ( F " A )  <->  E. x
( x  e.  A  /\  x F y ) )
469elima2 5341 . . . . . 6  |-  ( y  e.  ( F " B )  <->  E. x
( x  e.  B  /\  x F y ) )
4746notbii 296 . . . . 5  |-  ( -.  y  e.  ( F
" B )  <->  -.  E. x
( x  e.  B  /\  x F y ) )
4845, 47anbi12i 697 . . . 4  |-  ( ( y  e.  ( F
" A )  /\  -.  y  e.  ( F " B ) )  <-> 
( E. x ( x  e.  A  /\  x F y )  /\  -.  E. x ( x  e.  B  /\  x F y ) ) )
4941, 44, 483bitr4g 288 . . 3  |-  ( Fun  `' F  ->  ( E. x ( x  e.  ( A  \  B
)  /\  x F
y )  <->  ( y  e.  ( F " A
)  /\  -.  y  e.  ( F " B
) ) ) )
509elima2 5341 . . 3  |-  ( y  e.  ( F "
( A  \  B
) )  <->  E. x
( x  e.  ( A  \  B )  /\  x F y ) )
51 eldif 3486 . . 3  |-  ( y  e.  ( ( F
" A )  \ 
( F " B
) )  <->  ( y  e.  ( F " A
)  /\  -.  y  e.  ( F " B
) ) )
5249, 50, 513bitr4g 288 . 2  |-  ( Fun  `' F  ->  ( y  e.  ( F "
( A  \  B
) )  <->  y  e.  ( ( F " A )  \  ( F " B ) ) ) )
5352eqrdv 2464 1  |-  ( Fun  `' F  ->  ( F
" ( A  \  B ) )  =  ( ( F " A )  \  ( F " B ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 368    /\ wa 369   A.wal 1377    = wceq 1379   E.wex 1596    e. wcel 1767   E*wmo 2276    \ cdif 3473   class class class wbr 4447   `'ccnv 4998   "cima 5002   Fun wfun 5580
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pr 4686
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448  df-opab 4506  df-id 4795  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-fun 5588
This theorem is referenced by:  imain  5662  resdif  5834  difpreima  6007  domunsncan  7614  phplem4  7696  php3  7700  infdifsn  8069  cantnfp1lem3  8095  cantnfp1lem3OLD  8121  mapfienOLD  8134  enfin1ai  8760  fin1a2lem7  8782  symgfixelsi  16252  dprdf1o  16866  frlmlbs  18595  f1lindf  18621  cnclima  19532  iscncl  19533  qtopcld  19946  qtoprest  19950  qtopcmap  19952  mbfimaicc  21772  ismbf3d  21793  i1fd  21820  ballotlemfrc  28102
  Copyright terms: Public domain W3C validator