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

Theorem imadif 5676
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 836 . . . . . . . 8  |-  ( ( ( x  e.  A  /\  -.  x  e.  B
)  /\  x F
y )  <->  ( (
x  e.  A  /\  x F y )  /\  ( -.  x  e.  B  /\  x F y ) ) )
21exbii 1712 . . . . . . 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 1725 . . . . . . 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 198 . . . . . 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 1755 . . . . . . . . . . 11  |-  F/ x Fun  `' F
6 nfe1 1894 . . . . . . . . . . 11  |-  F/ x E. x ( x F y  /\  -.  x  e.  B )
75, 6nfan 1988 . . . . . . . . . 10  |-  F/ x
( Fun  `' F  /\  E. x ( x F y  /\  -.  x  e.  B )
)
8 funmo 5617 . . . . . . . . . . . . . 14  |-  ( Fun  `' F  ->  E* x  y `' F x )
9 vex 3083 . . . . . . . . . . . . . . . 16  |-  y  e. 
_V
10 vex 3083 . . . . . . . . . . . . . . . 16  |-  x  e. 
_V
119, 10brcnv 5036 . . . . . . . . . . . . . . 15  |-  ( y `' F x  <->  x F
y )
1211mobii 2292 . . . . . . . . . . . . . 14  |-  ( E* x  y `' F x 
<->  E* x  x F y )
138, 12sylib 199 . . . . . . . . . . . . 13  |-  ( Fun  `' F  ->  E* x  x F y )
14 mopick 2334 . . . . . . . . . . . . 13  |-  ( ( E* x  x F y  /\  E. x
( x F y  /\  -.  x  e.  B ) )  -> 
( x F y  ->  -.  x  e.  B ) )
1513, 14sylan 473 . . . . . . . . . . . 12  |-  ( ( Fun  `' F  /\  E. x ( x F y  /\  -.  x  e.  B ) )  -> 
( x F y  ->  -.  x  e.  B ) )
1615con2d 118 . . . . . . . . . . 11  |-  ( ( Fun  `' F  /\  E. x ( x F y  /\  -.  x  e.  B ) )  -> 
( x  e.  B  ->  -.  x F y ) )
17 imnan 423 . . . . . . . . . . 11  |-  ( ( x  e.  B  ->  -.  x F y )  <->  -.  ( x  e.  B  /\  x F y ) )
1816, 17sylib 199 . . . . . . . . . 10  |-  ( ( Fun  `' F  /\  E. x ( x F y  /\  -.  x  e.  B ) )  ->  -.  ( x  e.  B  /\  x F y ) )
197, 18alrimi 1932 . . . . . . . . 9  |-  ( ( Fun  `' F  /\  E. x ( x F y  /\  -.  x  e.  B ) )  ->  A. x  -.  (
x  e.  B  /\  x F y ) )
2019ex 435 . . . . . . . 8  |-  ( Fun  `' F  ->  ( E. x ( x F y  /\  -.  x  e.  B )  ->  A. x  -.  ( x  e.  B  /\  x F y ) ) )
21 exancom 1716 . . . . . . . 8  |-  ( E. x ( x F y  /\  -.  x  e.  B )  <->  E. x
( -.  x  e.  B  /\  x F y ) )
22 alnex 1659 . . . . . . . 8  |-  ( A. x  -.  ( x  e.  B  /\  x F y )  <->  -.  E. x
( x  e.  B  /\  x F y ) )
2320, 21, 223imtr3g 272 . . . . . . 7  |-  ( Fun  `' F  ->  ( E. x ( -.  x  e.  B  /\  x F y )  ->  -.  E. x ( x  e.  B  /\  x F y ) ) )
2423anim2d 567 . . . . . 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 33 . . . . 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 1730 . . . . . . 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 478 . . . . . 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 875 . . . . . . . 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 490 . . . . . . . . 9  |-  ( -.  ( x  e.  B  /\  x F y )  <-> 
( -.  x  e.  B  \/  -.  x F y ) )
3029anbi2i 698 . . . . . . . 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 805 . . . . . . . . 9  |-  ( ( ( x  e.  A  /\  -.  x  e.  B
)  /\  x F
y )  <->  ( (
x  e.  A  /\  x F y )  /\  -.  x  e.  B
) )
32 pm3.24 890 . . . . . . . . . . . 12  |-  -.  (
x F y  /\  -.  x F y )
3332intnan 922 . . . . . . . . . . 11  |-  -.  (
x  e.  A  /\  ( x F y  /\  -.  x F y ) )
34 anass 653 . . . . . . . . . . 11  |-  ( ( ( x  e.  A  /\  x F y )  /\  -.  x F y )  <->  ( x  e.  A  /\  (
x F y  /\  -.  x F y ) ) )
3533, 34mtbir 300 . . . . . . . . . 10  |-  -.  (
( x  e.  A  /\  x F y )  /\  -.  x F y )
3635biorfi 408 . . . . . . . . 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 252 . . . . . . . 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 280 . . . . . . 7  |-  ( ( ( x  e.  A  /\  x F y )  /\  -.  ( x  e.  B  /\  x F y ) )  <-> 
( ( x  e.  A  /\  -.  x  e.  B )  /\  x F y ) )
3938exbii 1712 . . . . . 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 199 . . . . 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 206 . . . 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 3446 . . . . . 6  |-  ( x  e.  ( A  \  B )  <->  ( x  e.  A  /\  -.  x  e.  B ) )
4342anbi1i 699 . . . . 5  |-  ( ( x  e.  ( A 
\  B )  /\  x F y )  <->  ( (
x  e.  A  /\  -.  x  e.  B
)  /\  x F
y ) )
4443exbii 1712 . . . 4  |-  ( E. x ( x  e.  ( A  \  B
)  /\  x F
y )  <->  E. x
( ( x  e.  A  /\  -.  x  e.  B )  /\  x F y ) )
459elima2 5193 . . . . 5  |-  ( y  e.  ( F " A )  <->  E. x
( x  e.  A  /\  x F y ) )
469elima2 5193 . . . . . 6  |-  ( y  e.  ( F " B )  <->  E. x
( x  e.  B  /\  x F y ) )
4746notbii 297 . . . . 5  |-  ( -.  y  e.  ( F
" B )  <->  -.  E. x
( x  e.  B  /\  x F y ) )
4845, 47anbi12i 701 . . . 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 291 . . 3  |-  ( Fun  `' F  ->  ( E. x ( x  e.  ( A  \  B
)  /\  x F
y )  <->  ( y  e.  ( F " A
)  /\  -.  y  e.  ( F " B
) ) ) )
509elima2 5193 . . 3  |-  ( y  e.  ( F "
( A  \  B
) )  <->  E. x
( x  e.  ( A  \  B )  /\  x F y ) )
51 eldif 3446 . . 3  |-  ( y  e.  ( ( F
" A )  \ 
( F " B
) )  <->  ( y  e.  ( F " A
)  /\  -.  y  e.  ( F " B
) ) )
5249, 50, 513bitr4g 291 . 2  |-  ( Fun  `' F  ->  ( y  e.  ( F "
( A  \  B
) )  <->  y  e.  ( ( F " A )  \  ( F " B ) ) ) )
5352eqrdv 2419 1  |-  ( Fun  `' F  ->  ( F
" ( A  \  B ) )  =  ( ( F " A )  \  ( F " B ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 369    /\ wa 370   A.wal 1435    = wceq 1437   E.wex 1657    e. wcel 1872   E*wmo 2270    \ cdif 3433   class class class wbr 4423   `'ccnv 4852   "cima 4856   Fun wfun 5595
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pr 4660
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-rab 2780  df-v 3082  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-sn 3999  df-pr 4001  df-op 4005  df-br 4424  df-opab 4483  df-id 4768  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-fun 5603
This theorem is referenced by:  imain  5677  resdif  5851  difpreima  6024  domunsncan  7682  phplem4  7764  php3  7768  infdifsn  8171  cantnfp1lem3  8194  enfin1ai  8822  fin1a2lem7  8844  symgfixelsi  17076  dprdf1o  17665  frlmlbs  19354  f1lindf  19379  cnclima  20283  iscncl  20284  qtopcld  20727  qtoprest  20731  qtopcmap  20733  mbfimaicc  22588  ismbf3d  22609  i1fd  22638  ballotlemfrc  29368  ballotlemfrcOLD  29406  poimirlem2  31907  poimirlem4  31909  poimirlem6  31911  poimirlem7  31912  poimirlem9  31914  poimirlem11  31916  poimirlem12  31917  poimirlem13  31918  poimirlem14  31919  poimirlem16  31921  poimirlem19  31924  poimirlem23  31928
  Copyright terms: Public domain W3C validator