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

Theorem imadif 6408
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 676 . . . . . . . 8 (((𝑥𝐴 ∧ ¬ 𝑥𝐵) ∧ 𝑥𝐹𝑦) ↔ ((𝑥𝐴𝑥𝐹𝑦) ∧ (¬ 𝑥𝐵𝑥𝐹𝑦)))
21exbii 1849 . . . . . . 7 (∃𝑥((𝑥𝐴 ∧ ¬ 𝑥𝐵) ∧ 𝑥𝐹𝑦) ↔ ∃𝑥((𝑥𝐴𝑥𝐹𝑦) ∧ (¬ 𝑥𝐵𝑥𝐹𝑦)))
3 19.40 1887 . . . . . . 7 (∃𝑥((𝑥𝐴𝑥𝐹𝑦) ∧ (¬ 𝑥𝐵𝑥𝐹𝑦)) → (∃𝑥(𝑥𝐴𝑥𝐹𝑦) ∧ ∃𝑥𝑥𝐵𝑥𝐹𝑦)))
42, 3sylbi 220 . . . . . 6 (∃𝑥((𝑥𝐴 ∧ ¬ 𝑥𝐵) ∧ 𝑥𝐹𝑦) → (∃𝑥(𝑥𝐴𝑥𝐹𝑦) ∧ ∃𝑥𝑥𝐵𝑥𝐹𝑦)))
5 nfv 1915 . . . . . . . . . . 11 𝑥Fun 𝐹
6 nfe1 2151 . . . . . . . . . . 11 𝑥𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥𝐵)
75, 6nfan 1900 . . . . . . . . . 10 𝑥(Fun 𝐹 ∧ ∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥𝐵))
8 funmo 6340 . . . . . . . . . . . . . 14 (Fun 𝐹 → ∃*𝑥 𝑦𝐹𝑥)
9 vex 3444 . . . . . . . . . . . . . . . 16 𝑦 ∈ V
10 vex 3444 . . . . . . . . . . . . . . . 16 𝑥 ∈ V
119, 10brcnv 5717 . . . . . . . . . . . . . . 15 (𝑦𝐹𝑥𝑥𝐹𝑦)
1211mobii 2606 . . . . . . . . . . . . . 14 (∃*𝑥 𝑦𝐹𝑥 ↔ ∃*𝑥 𝑥𝐹𝑦)
138, 12sylib 221 . . . . . . . . . . . . 13 (Fun 𝐹 → ∃*𝑥 𝑥𝐹𝑦)
14 mopick 2687 . . . . . . . . . . . . 13 ((∃*𝑥 𝑥𝐹𝑦 ∧ ∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥𝐵)) → (𝑥𝐹𝑦 → ¬ 𝑥𝐵))
1513, 14sylan 583 . . . . . . . . . . . 12 ((Fun 𝐹 ∧ ∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥𝐵)) → (𝑥𝐹𝑦 → ¬ 𝑥𝐵))
1615con2d 136 . . . . . . . . . . 11 ((Fun 𝐹 ∧ ∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥𝐵)) → (𝑥𝐵 → ¬ 𝑥𝐹𝑦))
17 imnan 403 . . . . . . . . . . 11 ((𝑥𝐵 → ¬ 𝑥𝐹𝑦) ↔ ¬ (𝑥𝐵𝑥𝐹𝑦))
1816, 17sylib 221 . . . . . . . . . 10 ((Fun 𝐹 ∧ ∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥𝐵)) → ¬ (𝑥𝐵𝑥𝐹𝑦))
197, 18alrimi 2211 . . . . . . . . 9 ((Fun 𝐹 ∧ ∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥𝐵)) → ∀𝑥 ¬ (𝑥𝐵𝑥𝐹𝑦))
2019ex 416 . . . . . . . 8 (Fun 𝐹 → (∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥𝐵) → ∀𝑥 ¬ (𝑥𝐵𝑥𝐹𝑦)))
21 exancom 1862 . . . . . . . 8 (∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥𝐵) ↔ ∃𝑥𝑥𝐵𝑥𝐹𝑦))
22 alnex 1783 . . . . . . . 8 (∀𝑥 ¬ (𝑥𝐵𝑥𝐹𝑦) ↔ ¬ ∃𝑥(𝑥𝐵𝑥𝐹𝑦))
2320, 21, 223imtr3g 298 . . . . . . 7 (Fun 𝐹 → (∃𝑥𝑥𝐵𝑥𝐹𝑦) → ¬ ∃𝑥(𝑥𝐵𝑥𝐹𝑦)))
2423anim2d 614 . . . . . 6 (Fun 𝐹 → ((∃𝑥(𝑥𝐴𝑥𝐹𝑦) ∧ ∃𝑥𝑥𝐵𝑥𝐹𝑦)) → (∃𝑥(𝑥𝐴𝑥𝐹𝑦) ∧ ¬ ∃𝑥(𝑥𝐵𝑥𝐹𝑦))))
254, 24syl5 34 . . . . 5 (Fun 𝐹 → (∃𝑥((𝑥𝐴 ∧ ¬ 𝑥𝐵) ∧ 𝑥𝐹𝑦) → (∃𝑥(𝑥𝐴𝑥𝐹𝑦) ∧ ¬ ∃𝑥(𝑥𝐵𝑥𝐹𝑦))))
26 19.29r 1875 . . . . . . 7 ((∃𝑥(𝑥𝐴𝑥𝐹𝑦) ∧ ∀𝑥 ¬ (𝑥𝐵𝑥𝐹𝑦)) → ∃𝑥((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ (𝑥𝐵𝑥𝐹𝑦)))
2722, 26sylan2br 597 . . . . . 6 ((∃𝑥(𝑥𝐴𝑥𝐹𝑦) ∧ ¬ ∃𝑥(𝑥𝐵𝑥𝐹𝑦)) → ∃𝑥((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ (𝑥𝐵𝑥𝐹𝑦)))
28 andi 1005 . . . . . . . 8 (((𝑥𝐴𝑥𝐹𝑦) ∧ (¬ 𝑥𝐵 ∨ ¬ 𝑥𝐹𝑦)) ↔ (((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ 𝑥𝐵) ∨ ((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ 𝑥𝐹𝑦)))
29 ianor 979 . . . . . . . . 9 (¬ (𝑥𝐵𝑥𝐹𝑦) ↔ (¬ 𝑥𝐵 ∨ ¬ 𝑥𝐹𝑦))
3029anbi2i 625 . . . . . . . 8 (((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ (𝑥𝐵𝑥𝐹𝑦)) ↔ ((𝑥𝐴𝑥𝐹𝑦) ∧ (¬ 𝑥𝐵 ∨ ¬ 𝑥𝐹𝑦)))
31 an32 645 . . . . . . . . 9 (((𝑥𝐴 ∧ ¬ 𝑥𝐵) ∧ 𝑥𝐹𝑦) ↔ ((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ 𝑥𝐵))
32 pm3.24 406 . . . . . . . . . . . 12 ¬ (𝑥𝐹𝑦 ∧ ¬ 𝑥𝐹𝑦)
3332intnan 490 . . . . . . . . . . 11 ¬ (𝑥𝐴 ∧ (𝑥𝐹𝑦 ∧ ¬ 𝑥𝐹𝑦))
34 anass 472 . . . . . . . . . . 11 (((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ 𝑥𝐹𝑦) ↔ (𝑥𝐴 ∧ (𝑥𝐹𝑦 ∧ ¬ 𝑥𝐹𝑦)))
3533, 34mtbir 326 . . . . . . . . . 10 ¬ ((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ 𝑥𝐹𝑦)
3635biorfi 936 . . . . . . . . 9 (((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ 𝑥𝐵) ↔ (((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ 𝑥𝐵) ∨ ((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ 𝑥𝐹𝑦)))
3731, 36bitri 278 . . . . . . . 8 (((𝑥𝐴 ∧ ¬ 𝑥𝐵) ∧ 𝑥𝐹𝑦) ↔ (((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ 𝑥𝐵) ∨ ((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ 𝑥𝐹𝑦)))
3828, 30, 373bitr4i 306 . . . . . . 7 (((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ (𝑥𝐵𝑥𝐹𝑦)) ↔ ((𝑥𝐴 ∧ ¬ 𝑥𝐵) ∧ 𝑥𝐹𝑦))
3938exbii 1849 . . . . . 6 (∃𝑥((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ (𝑥𝐵𝑥𝐹𝑦)) ↔ ∃𝑥((𝑥𝐴 ∧ ¬ 𝑥𝐵) ∧ 𝑥𝐹𝑦))
4027, 39sylib 221 . . . . 5 ((∃𝑥(𝑥𝐴𝑥𝐹𝑦) ∧ ¬ ∃𝑥(𝑥𝐵𝑥𝐹𝑦)) → ∃𝑥((𝑥𝐴 ∧ ¬ 𝑥𝐵) ∧ 𝑥𝐹𝑦))
4125, 40impbid1 228 . . . 4 (Fun 𝐹 → (∃𝑥((𝑥𝐴 ∧ ¬ 𝑥𝐵) ∧ 𝑥𝐹𝑦) ↔ (∃𝑥(𝑥𝐴𝑥𝐹𝑦) ∧ ¬ ∃𝑥(𝑥𝐵𝑥𝐹𝑦))))
42 eldif 3891 . . . . . 6 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐵))
4342anbi1i 626 . . . . 5 ((𝑥 ∈ (𝐴𝐵) ∧ 𝑥𝐹𝑦) ↔ ((𝑥𝐴 ∧ ¬ 𝑥𝐵) ∧ 𝑥𝐹𝑦))
4443exbii 1849 . . . 4 (∃𝑥(𝑥 ∈ (𝐴𝐵) ∧ 𝑥𝐹𝑦) ↔ ∃𝑥((𝑥𝐴 ∧ ¬ 𝑥𝐵) ∧ 𝑥𝐹𝑦))
459elima2 5902 . . . . 5 (𝑦 ∈ (𝐹𝐴) ↔ ∃𝑥(𝑥𝐴𝑥𝐹𝑦))
469elima2 5902 . . . . . 6 (𝑦 ∈ (𝐹𝐵) ↔ ∃𝑥(𝑥𝐵𝑥𝐹𝑦))
4746notbii 323 . . . . 5 𝑦 ∈ (𝐹𝐵) ↔ ¬ ∃𝑥(𝑥𝐵𝑥𝐹𝑦))
4845, 47anbi12i 629 . . . 4 ((𝑦 ∈ (𝐹𝐴) ∧ ¬ 𝑦 ∈ (𝐹𝐵)) ↔ (∃𝑥(𝑥𝐴𝑥𝐹𝑦) ∧ ¬ ∃𝑥(𝑥𝐵𝑥𝐹𝑦)))
4941, 44, 483bitr4g 317 . . 3 (Fun 𝐹 → (∃𝑥(𝑥 ∈ (𝐴𝐵) ∧ 𝑥𝐹𝑦) ↔ (𝑦 ∈ (𝐹𝐴) ∧ ¬ 𝑦 ∈ (𝐹𝐵))))
509elima2 5902 . . 3 (𝑦 ∈ (𝐹 “ (𝐴𝐵)) ↔ ∃𝑥(𝑥 ∈ (𝐴𝐵) ∧ 𝑥𝐹𝑦))
51 eldif 3891 . . 3 (𝑦 ∈ ((𝐹𝐴) ∖ (𝐹𝐵)) ↔ (𝑦 ∈ (𝐹𝐴) ∧ ¬ 𝑦 ∈ (𝐹𝐵)))
5249, 50, 513bitr4g 317 . 2 (Fun 𝐹 → (𝑦 ∈ (𝐹 “ (𝐴𝐵)) ↔ 𝑦 ∈ ((𝐹𝐴) ∖ (𝐹𝐵))))
5352eqrdv 2796 1 (Fun 𝐹 → (𝐹 “ (𝐴𝐵)) = ((𝐹𝐴) ∖ (𝐹𝐵)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 399  wo 844  wal 1536   = wceq 1538  wex 1781  wcel 2111  ∃*wmo 2596  cdif 3878   class class class wbr 5030  ccnv 5518  cima 5522  Fun wfun 6318
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-opab 5093  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-fun 6326
This theorem is referenced by:  imain  6409  resdif  6610  difpreima  6812  domunsncan  8600  phplem4  8683  php3  8687  infdifsn  9104  cantnfp1lem3  9127  enfin1ai  9795  fin1a2lem7  9817  symgfixelsi  18555  dprdf1o  19147  frlmlbs  20486  f1lindf  20511  cnclima  21873  iscncl  21874  qtopcld  22318  qtoprest  22322  qtopcmap  22324  mbfimaicc  24235  ismbf3d  24258  i1fd  24285  ballotlemfrc  31894  poimirlem2  35059  poimirlem4  35061  poimirlem6  35063  poimirlem7  35064  poimirlem9  35066  poimirlem11  35068  poimirlem12  35069  poimirlem13  35070  poimirlem14  35071  poimirlem16  35073  poimirlem19  35076  poimirlem23  35080
  Copyright terms: Public domain W3C validator