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

Theorem imadif 6635
Description: The image of a difference is the difference of images. (Contributed by NM, 24-May-1998.)
Assertion
Ref Expression
imadif (Fun 𝐹 → (𝐹 “ (𝐴𝐵)) = ((𝐹𝐴) ∖ (𝐹𝐵)))

Proof of Theorem imadif
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 anandir 675 . . . . . . . 8 (((𝑥𝐴 ∧ ¬ 𝑥𝐵) ∧ 𝑥𝐹𝑦) ↔ ((𝑥𝐴𝑥𝐹𝑦) ∧ (¬ 𝑥𝐵𝑥𝐹𝑦)))
21exbii 1843 . . . . . . 7 (∃𝑥((𝑥𝐴 ∧ ¬ 𝑥𝐵) ∧ 𝑥𝐹𝑦) ↔ ∃𝑥((𝑥𝐴𝑥𝐹𝑦) ∧ (¬ 𝑥𝐵𝑥𝐹𝑦)))
3 19.40 1882 . . . . . . 7 (∃𝑥((𝑥𝐴𝑥𝐹𝑦) ∧ (¬ 𝑥𝐵𝑥𝐹𝑦)) → (∃𝑥(𝑥𝐴𝑥𝐹𝑦) ∧ ∃𝑥𝑥𝐵𝑥𝐹𝑦)))
42, 3sylbi 216 . . . . . 6 (∃𝑥((𝑥𝐴 ∧ ¬ 𝑥𝐵) ∧ 𝑥𝐹𝑦) → (∃𝑥(𝑥𝐴𝑥𝐹𝑦) ∧ ∃𝑥𝑥𝐵𝑥𝐹𝑦)))
5 nfv 1910 . . . . . . . . . . 11 𝑥Fun 𝐹
6 nfe1 2140 . . . . . . . . . . 11 𝑥𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥𝐵)
75, 6nfan 1895 . . . . . . . . . 10 𝑥(Fun 𝐹 ∧ ∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥𝐵))
8 funmo 6566 . . . . . . . . . . . . . 14 (Fun 𝐹 → ∃*𝑥 𝑦𝐹𝑥)
9 vex 3466 . . . . . . . . . . . . . . . 16 𝑦 ∈ V
10 vex 3466 . . . . . . . . . . . . . . . 16 𝑥 ∈ V
119, 10brcnv 5881 . . . . . . . . . . . . . . 15 (𝑦𝐹𝑥𝑥𝐹𝑦)
1211mobii 2537 . . . . . . . . . . . . . 14 (∃*𝑥 𝑦𝐹𝑥 ↔ ∃*𝑥 𝑥𝐹𝑦)
138, 12sylib 217 . . . . . . . . . . . . 13 (Fun 𝐹 → ∃*𝑥 𝑥𝐹𝑦)
14 mopick 2614 . . . . . . . . . . . . 13 ((∃*𝑥 𝑥𝐹𝑦 ∧ ∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥𝐵)) → (𝑥𝐹𝑦 → ¬ 𝑥𝐵))
1513, 14sylan 578 . . . . . . . . . . . 12 ((Fun 𝐹 ∧ ∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥𝐵)) → (𝑥𝐹𝑦 → ¬ 𝑥𝐵))
1615con2d 134 . . . . . . . . . . 11 ((Fun 𝐹 ∧ ∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥𝐵)) → (𝑥𝐵 → ¬ 𝑥𝐹𝑦))
17 imnan 398 . . . . . . . . . . 11 ((𝑥𝐵 → ¬ 𝑥𝐹𝑦) ↔ ¬ (𝑥𝐵𝑥𝐹𝑦))
1816, 17sylib 217 . . . . . . . . . 10 ((Fun 𝐹 ∧ ∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥𝐵)) → ¬ (𝑥𝐵𝑥𝐹𝑦))
197, 18alrimi 2202 . . . . . . . . 9 ((Fun 𝐹 ∧ ∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥𝐵)) → ∀𝑥 ¬ (𝑥𝐵𝑥𝐹𝑦))
2019ex 411 . . . . . . . 8 (Fun 𝐹 → (∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥𝐵) → ∀𝑥 ¬ (𝑥𝐵𝑥𝐹𝑦)))
21 exancom 1857 . . . . . . . 8 (∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥𝐵) ↔ ∃𝑥𝑥𝐵𝑥𝐹𝑦))
22 alnex 1776 . . . . . . . 8 (∀𝑥 ¬ (𝑥𝐵𝑥𝐹𝑦) ↔ ¬ ∃𝑥(𝑥𝐵𝑥𝐹𝑦))
2320, 21, 223imtr3g 294 . . . . . . 7 (Fun 𝐹 → (∃𝑥𝑥𝐵𝑥𝐹𝑦) → ¬ ∃𝑥(𝑥𝐵𝑥𝐹𝑦)))
2423anim2d 610 . . . . . 6 (Fun 𝐹 → ((∃𝑥(𝑥𝐴𝑥𝐹𝑦) ∧ ∃𝑥𝑥𝐵𝑥𝐹𝑦)) → (∃𝑥(𝑥𝐴𝑥𝐹𝑦) ∧ ¬ ∃𝑥(𝑥𝐵𝑥𝐹𝑦))))
254, 24syl5 34 . . . . 5 (Fun 𝐹 → (∃𝑥((𝑥𝐴 ∧ ¬ 𝑥𝐵) ∧ 𝑥𝐹𝑦) → (∃𝑥(𝑥𝐴𝑥𝐹𝑦) ∧ ¬ ∃𝑥(𝑥𝐵𝑥𝐹𝑦))))
26 19.29r 1870 . . . . . . 7 ((∃𝑥(𝑥𝐴𝑥𝐹𝑦) ∧ ∀𝑥 ¬ (𝑥𝐵𝑥𝐹𝑦)) → ∃𝑥((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ (𝑥𝐵𝑥𝐹𝑦)))
2722, 26sylan2br 593 . . . . . 6 ((∃𝑥(𝑥𝐴𝑥𝐹𝑦) ∧ ¬ ∃𝑥(𝑥𝐵𝑥𝐹𝑦)) → ∃𝑥((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ (𝑥𝐵𝑥𝐹𝑦)))
28 andi 1005 . . . . . . . 8 (((𝑥𝐴𝑥𝐹𝑦) ∧ (¬ 𝑥𝐵 ∨ ¬ 𝑥𝐹𝑦)) ↔ (((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ 𝑥𝐵) ∨ ((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ 𝑥𝐹𝑦)))
29 ianor 979 . . . . . . . . 9 (¬ (𝑥𝐵𝑥𝐹𝑦) ↔ (¬ 𝑥𝐵 ∨ ¬ 𝑥𝐹𝑦))
3029anbi2i 621 . . . . . . . 8 (((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ (𝑥𝐵𝑥𝐹𝑦)) ↔ ((𝑥𝐴𝑥𝐹𝑦) ∧ (¬ 𝑥𝐵 ∨ ¬ 𝑥𝐹𝑦)))
31 an32 644 . . . . . . . . 9 (((𝑥𝐴 ∧ ¬ 𝑥𝐵) ∧ 𝑥𝐹𝑦) ↔ ((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ 𝑥𝐵))
32 pm3.24 401 . . . . . . . . . . . 12 ¬ (𝑥𝐹𝑦 ∧ ¬ 𝑥𝐹𝑦)
3332intnan 485 . . . . . . . . . . 11 ¬ (𝑥𝐴 ∧ (𝑥𝐹𝑦 ∧ ¬ 𝑥𝐹𝑦))
34 anass 467 . . . . . . . . . . 11 (((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ 𝑥𝐹𝑦) ↔ (𝑥𝐴 ∧ (𝑥𝐹𝑦 ∧ ¬ 𝑥𝐹𝑦)))
3533, 34mtbir 322 . . . . . . . . . 10 ¬ ((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ 𝑥𝐹𝑦)
3635biorfi 936 . . . . . . . . 9 (((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ 𝑥𝐵) ↔ (((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ 𝑥𝐵) ∨ ((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ 𝑥𝐹𝑦)))
3731, 36bitri 274 . . . . . . . 8 (((𝑥𝐴 ∧ ¬ 𝑥𝐵) ∧ 𝑥𝐹𝑦) ↔ (((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ 𝑥𝐵) ∨ ((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ 𝑥𝐹𝑦)))
3828, 30, 373bitr4i 302 . . . . . . 7 (((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ (𝑥𝐵𝑥𝐹𝑦)) ↔ ((𝑥𝐴 ∧ ¬ 𝑥𝐵) ∧ 𝑥𝐹𝑦))
3938exbii 1843 . . . . . 6 (∃𝑥((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ (𝑥𝐵𝑥𝐹𝑦)) ↔ ∃𝑥((𝑥𝐴 ∧ ¬ 𝑥𝐵) ∧ 𝑥𝐹𝑦))
4027, 39sylib 217 . . . . 5 ((∃𝑥(𝑥𝐴𝑥𝐹𝑦) ∧ ¬ ∃𝑥(𝑥𝐵𝑥𝐹𝑦)) → ∃𝑥((𝑥𝐴 ∧ ¬ 𝑥𝐵) ∧ 𝑥𝐹𝑦))
4125, 40impbid1 224 . . . 4 (Fun 𝐹 → (∃𝑥((𝑥𝐴 ∧ ¬ 𝑥𝐵) ∧ 𝑥𝐹𝑦) ↔ (∃𝑥(𝑥𝐴𝑥𝐹𝑦) ∧ ¬ ∃𝑥(𝑥𝐵𝑥𝐹𝑦))))
42 eldif 3956 . . . . . 6 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐵))
4342anbi1i 622 . . . . 5 ((𝑥 ∈ (𝐴𝐵) ∧ 𝑥𝐹𝑦) ↔ ((𝑥𝐴 ∧ ¬ 𝑥𝐵) ∧ 𝑥𝐹𝑦))
4443exbii 1843 . . . 4 (∃𝑥(𝑥 ∈ (𝐴𝐵) ∧ 𝑥𝐹𝑦) ↔ ∃𝑥((𝑥𝐴 ∧ ¬ 𝑥𝐵) ∧ 𝑥𝐹𝑦))
459elima2 6067 . . . . 5 (𝑦 ∈ (𝐹𝐴) ↔ ∃𝑥(𝑥𝐴𝑥𝐹𝑦))
469elima2 6067 . . . . . 6 (𝑦 ∈ (𝐹𝐵) ↔ ∃𝑥(𝑥𝐵𝑥𝐹𝑦))
4746notbii 319 . . . . 5 𝑦 ∈ (𝐹𝐵) ↔ ¬ ∃𝑥(𝑥𝐵𝑥𝐹𝑦))
4845, 47anbi12i 626 . . . 4 ((𝑦 ∈ (𝐹𝐴) ∧ ¬ 𝑦 ∈ (𝐹𝐵)) ↔ (∃𝑥(𝑥𝐴𝑥𝐹𝑦) ∧ ¬ ∃𝑥(𝑥𝐵𝑥𝐹𝑦)))
4941, 44, 483bitr4g 313 . . 3 (Fun 𝐹 → (∃𝑥(𝑥 ∈ (𝐴𝐵) ∧ 𝑥𝐹𝑦) ↔ (𝑦 ∈ (𝐹𝐴) ∧ ¬ 𝑦 ∈ (𝐹𝐵))))
509elima2 6067 . . 3 (𝑦 ∈ (𝐹 “ (𝐴𝐵)) ↔ ∃𝑥(𝑥 ∈ (𝐴𝐵) ∧ 𝑥𝐹𝑦))
51 eldif 3956 . . 3 (𝑦 ∈ ((𝐹𝐴) ∖ (𝐹𝐵)) ↔ (𝑦 ∈ (𝐹𝐴) ∧ ¬ 𝑦 ∈ (𝐹𝐵)))
5249, 50, 513bitr4g 313 . 2 (Fun 𝐹 → (𝑦 ∈ (𝐹 “ (𝐴𝐵)) ↔ 𝑦 ∈ ((𝐹𝐴) ∖ (𝐹𝐵))))
5352eqrdv 2724 1 (Fun 𝐹 → (𝐹 “ (𝐴𝐵)) = ((𝐹𝐴) ∖ (𝐹𝐵)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 394  wo 845  wal 1532   = wceq 1534  wex 1774  wcel 2099  ∃*wmo 2527  cdif 3943   class class class wbr 5145  ccnv 5673  cima 5677  Fun wfun 6540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-12 2167  ax-ext 2697  ax-sep 5296  ax-nul 5303  ax-pr 5425
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-clab 2704  df-cleq 2718  df-clel 2803  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3464  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-nul 4323  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-br 5146  df-opab 5208  df-id 5572  df-xp 5680  df-rel 5681  df-cnv 5682  df-co 5683  df-dm 5684  df-rn 5685  df-res 5686  df-ima 5687  df-fun 6548
This theorem is referenced by:  imain  6636  resdif  6856  difpreima  7070  domunsncan  9102  phplem2  9235  php3  9239  phplem4OLD  9247  php3OLD  9251  infdifsn  9693  cantnfp1lem3  9716  enfin1ai  10418  fin1a2lem7  10440  symgfixelsi  19429  dprdf1o  20028  frlmlbs  21791  f1lindf  21816  cnclima  23260  iscncl  23261  qtopcld  23705  qtoprest  23709  qtopcmap  23711  mbfimaicc  25648  ismbf3d  25671  i1fd  25698  ballotlemfrc  34373  poimirlem2  37336  poimirlem4  37338  poimirlem6  37340  poimirlem7  37341  poimirlem9  37343  poimirlem11  37345  poimirlem12  37346  poimirlem13  37347  poimirlem14  37348  poimirlem16  37350  poimirlem19  37353  poimirlem23  37357
  Copyright terms: Public domain W3C validator