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

Theorem imadif 5669
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 829 . . . . . . . 8  |-  ( ( ( x  e.  A  /\  -.  x  e.  B
)  /\  x F
y )  <->  ( (
x  e.  A  /\  x F y )  /\  ( -.  x  e.  B  /\  x F y ) ) )
21exbii 1668 . . . . . . 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 1680 . . . . . . 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 1708 . . . . . . . . . . 11  |-  F/ x Fun  `' F
6 nfe1 1841 . . . . . . . . . . 11  |-  F/ x E. x ( x F y  /\  -.  x  e.  B )
75, 6nfan 1929 . . . . . . . . . 10  |-  F/ x
( Fun  `' F  /\  E. x ( x F y  /\  -.  x  e.  B )
)
8 funmo 5610 . . . . . . . . . . . . . 14  |-  ( Fun  `' F  ->  E* x  y `' F x )
9 vex 3112 . . . . . . . . . . . . . . . 16  |-  y  e. 
_V
10 vex 3112 . . . . . . . . . . . . . . . 16  |-  x  e. 
_V
119, 10brcnv 5195 . . . . . . . . . . . . . . 15  |-  ( y `' F x  <->  x F
y )
1211mobii 2308 . . . . . . . . . . . . . 14  |-  ( E* x  y `' F x 
<->  E* x  x F y )
138, 12sylib 196 . . . . . . . . . . . . 13  |-  ( Fun  `' F  ->  E* x  x F y )
14 mopick 2356 . . . . . . . . . . . . 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 1878 . . . . . . . . 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 1672 . . . . . . . 8  |-  ( E. x ( x F y  /\  -.  x  e.  B )  <->  E. x
( -.  x  e.  B  /\  x F y ) )
22 alnex 1615 . . . . . . . 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 1685 . . . . . . 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 867 . . . . . . . 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 798 . . . . . . . . 9  |-  ( ( ( x  e.  A  /\  -.  x  e.  B
)  /\  x F
y )  <->  ( (
x  e.  A  /\  x F y )  /\  -.  x  e.  B
) )
32 pm3.24 882 . . . . . . . . . . . 12  |-  -.  (
x F y  /\  -.  x F y )
3332intnan 914 . . . . . . . . . . 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 1668 . . . . . 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 3481 . . . . . 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 1668 . . . 4  |-  ( E. x ( x  e.  ( A  \  B
)  /\  x F
y )  <->  E. x
( ( x  e.  A  /\  -.  x  e.  B )  /\  x F y ) )
459elima2 5353 . . . . 5  |-  ( y  e.  ( F " A )  <->  E. x
( x  e.  A  /\  x F y ) )
469elima2 5353 . . . . . 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 5353 . . 3  |-  ( y  e.  ( F "
( A  \  B
) )  <->  E. x
( x  e.  ( A  \  B )  /\  x F y ) )
51 eldif 3481 . . 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 2454 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 1393    = wceq 1395   E.wex 1613    e. wcel 1819   E*wmo 2284    \ cdif 3468   class class class wbr 4456   `'ccnv 5007   "cima 5011   Fun wfun 5588
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-sep 4578  ax-nul 4586  ax-pr 4695
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-sn 4033  df-pr 4035  df-op 4039  df-br 4457  df-opab 4516  df-id 4804  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-rn 5019  df-res 5020  df-ima 5021  df-fun 5596
This theorem is referenced by:  imain  5670  resdif  5842  difpreima  6016  domunsncan  7636  phplem4  7718  php3  7722  infdifsn  8090  cantnfp1lem3  8116  cantnfp1lem3OLD  8142  mapfienOLD  8155  enfin1ai  8781  fin1a2lem7  8803  symgfixelsi  16586  dprdf1o  17205  frlmlbs  18957  f1lindf  18983  cnclima  19895  iscncl  19896  qtopcld  20339  qtoprest  20343  qtopcmap  20345  mbfimaicc  22165  ismbf3d  22186  i1fd  22213  ballotlemfrc  28640
  Copyright terms: Public domain W3C validator