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

Theorem imadif 6585
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 1850 . . . . . . 7 (∃𝑥((𝑥𝐴 ∧ ¬ 𝑥𝐵) ∧ 𝑥𝐹𝑦) ↔ ∃𝑥((𝑥𝐴𝑥𝐹𝑦) ∧ (¬ 𝑥𝐵𝑥𝐹𝑦)))
3 19.40 1889 . . . . . . 7 (∃𝑥((𝑥𝐴𝑥𝐹𝑦) ∧ (¬ 𝑥𝐵𝑥𝐹𝑦)) → (∃𝑥(𝑥𝐴𝑥𝐹𝑦) ∧ ∃𝑥𝑥𝐵𝑥𝐹𝑦)))
42, 3sylbi 216 . . . . . 6 (∃𝑥((𝑥𝐴 ∧ ¬ 𝑥𝐵) ∧ 𝑥𝐹𝑦) → (∃𝑥(𝑥𝐴𝑥𝐹𝑦) ∧ ∃𝑥𝑥𝐵𝑥𝐹𝑦)))
5 nfv 1917 . . . . . . . . . . 11 𝑥Fun 𝐹
6 nfe1 2147 . . . . . . . . . . 11 𝑥𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥𝐵)
75, 6nfan 1902 . . . . . . . . . 10 𝑥(Fun 𝐹 ∧ ∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥𝐵))
8 funmo 6516 . . . . . . . . . . . . . 14 (Fun 𝐹 → ∃*𝑥 𝑦𝐹𝑥)
9 vex 3449 . . . . . . . . . . . . . . . 16 𝑦 ∈ V
10 vex 3449 . . . . . . . . . . . . . . . 16 𝑥 ∈ V
119, 10brcnv 5838 . . . . . . . . . . . . . . 15 (𝑦𝐹𝑥𝑥𝐹𝑦)
1211mobii 2546 . . . . . . . . . . . . . 14 (∃*𝑥 𝑦𝐹𝑥 ↔ ∃*𝑥 𝑥𝐹𝑦)
138, 12sylib 217 . . . . . . . . . . . . 13 (Fun 𝐹 → ∃*𝑥 𝑥𝐹𝑦)
14 mopick 2625 . . . . . . . . . . . . 13 ((∃*𝑥 𝑥𝐹𝑦 ∧ ∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥𝐵)) → (𝑥𝐹𝑦 → ¬ 𝑥𝐵))
1513, 14sylan 580 . . . . . . . . . . . 12 ((Fun 𝐹 ∧ ∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥𝐵)) → (𝑥𝐹𝑦 → ¬ 𝑥𝐵))
1615con2d 134 . . . . . . . . . . 11 ((Fun 𝐹 ∧ ∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥𝐵)) → (𝑥𝐵 → ¬ 𝑥𝐹𝑦))
17 imnan 400 . . . . . . . . . . 11 ((𝑥𝐵 → ¬ 𝑥𝐹𝑦) ↔ ¬ (𝑥𝐵𝑥𝐹𝑦))
1816, 17sylib 217 . . . . . . . . . 10 ((Fun 𝐹 ∧ ∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥𝐵)) → ¬ (𝑥𝐵𝑥𝐹𝑦))
197, 18alrimi 2206 . . . . . . . . 9 ((Fun 𝐹 ∧ ∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥𝐵)) → ∀𝑥 ¬ (𝑥𝐵𝑥𝐹𝑦))
2019ex 413 . . . . . . . 8 (Fun 𝐹 → (∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥𝐵) → ∀𝑥 ¬ (𝑥𝐵𝑥𝐹𝑦)))
21 exancom 1864 . . . . . . . 8 (∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥𝐵) ↔ ∃𝑥𝑥𝐵𝑥𝐹𝑦))
22 alnex 1783 . . . . . . . 8 (∀𝑥 ¬ (𝑥𝐵𝑥𝐹𝑦) ↔ ¬ ∃𝑥(𝑥𝐵𝑥𝐹𝑦))
2320, 21, 223imtr3g 294 . . . . . . 7 (Fun 𝐹 → (∃𝑥𝑥𝐵𝑥𝐹𝑦) → ¬ ∃𝑥(𝑥𝐵𝑥𝐹𝑦)))
2423anim2d 612 . . . . . 6 (Fun 𝐹 → ((∃𝑥(𝑥𝐴𝑥𝐹𝑦) ∧ ∃𝑥𝑥𝐵𝑥𝐹𝑦)) → (∃𝑥(𝑥𝐴𝑥𝐹𝑦) ∧ ¬ ∃𝑥(𝑥𝐵𝑥𝐹𝑦))))
254, 24syl5 34 . . . . 5 (Fun 𝐹 → (∃𝑥((𝑥𝐴 ∧ ¬ 𝑥𝐵) ∧ 𝑥𝐹𝑦) → (∃𝑥(𝑥𝐴𝑥𝐹𝑦) ∧ ¬ ∃𝑥(𝑥𝐵𝑥𝐹𝑦))))
26 19.29r 1877 . . . . . . 7 ((∃𝑥(𝑥𝐴𝑥𝐹𝑦) ∧ ∀𝑥 ¬ (𝑥𝐵𝑥𝐹𝑦)) → ∃𝑥((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ (𝑥𝐵𝑥𝐹𝑦)))
2722, 26sylan2br 595 . . . . . 6 ((∃𝑥(𝑥𝐴𝑥𝐹𝑦) ∧ ¬ ∃𝑥(𝑥𝐵𝑥𝐹𝑦)) → ∃𝑥((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ (𝑥𝐵𝑥𝐹𝑦)))
28 andi 1006 . . . . . . . 8 (((𝑥𝐴𝑥𝐹𝑦) ∧ (¬ 𝑥𝐵 ∨ ¬ 𝑥𝐹𝑦)) ↔ (((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ 𝑥𝐵) ∨ ((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ 𝑥𝐹𝑦)))
29 ianor 980 . . . . . . . . 9 (¬ (𝑥𝐵𝑥𝐹𝑦) ↔ (¬ 𝑥𝐵 ∨ ¬ 𝑥𝐹𝑦))
3029anbi2i 623 . . . . . . . 8 (((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ (𝑥𝐵𝑥𝐹𝑦)) ↔ ((𝑥𝐴𝑥𝐹𝑦) ∧ (¬ 𝑥𝐵 ∨ ¬ 𝑥𝐹𝑦)))
31 an32 644 . . . . . . . . 9 (((𝑥𝐴 ∧ ¬ 𝑥𝐵) ∧ 𝑥𝐹𝑦) ↔ ((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ 𝑥𝐵))
32 pm3.24 403 . . . . . . . . . . . 12 ¬ (𝑥𝐹𝑦 ∧ ¬ 𝑥𝐹𝑦)
3332intnan 487 . . . . . . . . . . 11 ¬ (𝑥𝐴 ∧ (𝑥𝐹𝑦 ∧ ¬ 𝑥𝐹𝑦))
34 anass 469 . . . . . . . . . . 11 (((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ 𝑥𝐹𝑦) ↔ (𝑥𝐴 ∧ (𝑥𝐹𝑦 ∧ ¬ 𝑥𝐹𝑦)))
3533, 34mtbir 322 . . . . . . . . . 10 ¬ ((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ 𝑥𝐹𝑦)
3635biorfi 937 . . . . . . . . 9 (((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ 𝑥𝐵) ↔ (((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ 𝑥𝐵) ∨ ((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ 𝑥𝐹𝑦)))
3731, 36bitri 274 . . . . . . . 8 (((𝑥𝐴 ∧ ¬ 𝑥𝐵) ∧ 𝑥𝐹𝑦) ↔ (((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ 𝑥𝐵) ∨ ((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ 𝑥𝐹𝑦)))
3828, 30, 373bitr4i 302 . . . . . . 7 (((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ (𝑥𝐵𝑥𝐹𝑦)) ↔ ((𝑥𝐴 ∧ ¬ 𝑥𝐵) ∧ 𝑥𝐹𝑦))
3938exbii 1850 . . . . . 6 (∃𝑥((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ (𝑥𝐵𝑥𝐹𝑦)) ↔ ∃𝑥((𝑥𝐴 ∧ ¬ 𝑥𝐵) ∧ 𝑥𝐹𝑦))
4027, 39sylib 217 . . . . 5 ((∃𝑥(𝑥𝐴𝑥𝐹𝑦) ∧ ¬ ∃𝑥(𝑥𝐵𝑥𝐹𝑦)) → ∃𝑥((𝑥𝐴 ∧ ¬ 𝑥𝐵) ∧ 𝑥𝐹𝑦))
4125, 40impbid1 224 . . . 4 (Fun 𝐹 → (∃𝑥((𝑥𝐴 ∧ ¬ 𝑥𝐵) ∧ 𝑥𝐹𝑦) ↔ (∃𝑥(𝑥𝐴𝑥𝐹𝑦) ∧ ¬ ∃𝑥(𝑥𝐵𝑥𝐹𝑦))))
42 eldif 3920 . . . . . 6 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐵))
4342anbi1i 624 . . . . 5 ((𝑥 ∈ (𝐴𝐵) ∧ 𝑥𝐹𝑦) ↔ ((𝑥𝐴 ∧ ¬ 𝑥𝐵) ∧ 𝑥𝐹𝑦))
4443exbii 1850 . . . 4 (∃𝑥(𝑥 ∈ (𝐴𝐵) ∧ 𝑥𝐹𝑦) ↔ ∃𝑥((𝑥𝐴 ∧ ¬ 𝑥𝐵) ∧ 𝑥𝐹𝑦))
459elima2 6019 . . . . 5 (𝑦 ∈ (𝐹𝐴) ↔ ∃𝑥(𝑥𝐴𝑥𝐹𝑦))
469elima2 6019 . . . . . 6 (𝑦 ∈ (𝐹𝐵) ↔ ∃𝑥(𝑥𝐵𝑥𝐹𝑦))
4746notbii 319 . . . . 5 𝑦 ∈ (𝐹𝐵) ↔ ¬ ∃𝑥(𝑥𝐵𝑥𝐹𝑦))
4845, 47anbi12i 627 . . . 4 ((𝑦 ∈ (𝐹𝐴) ∧ ¬ 𝑦 ∈ (𝐹𝐵)) ↔ (∃𝑥(𝑥𝐴𝑥𝐹𝑦) ∧ ¬ ∃𝑥(𝑥𝐵𝑥𝐹𝑦)))
4941, 44, 483bitr4g 313 . . 3 (Fun 𝐹 → (∃𝑥(𝑥 ∈ (𝐴𝐵) ∧ 𝑥𝐹𝑦) ↔ (𝑦 ∈ (𝐹𝐴) ∧ ¬ 𝑦 ∈ (𝐹𝐵))))
509elima2 6019 . . 3 (𝑦 ∈ (𝐹 “ (𝐴𝐵)) ↔ ∃𝑥(𝑥 ∈ (𝐴𝐵) ∧ 𝑥𝐹𝑦))
51 eldif 3920 . . 3 (𝑦 ∈ ((𝐹𝐴) ∖ (𝐹𝐵)) ↔ (𝑦 ∈ (𝐹𝐴) ∧ ¬ 𝑦 ∈ (𝐹𝐵)))
5249, 50, 513bitr4g 313 . 2 (Fun 𝐹 → (𝑦 ∈ (𝐹 “ (𝐴𝐵)) ↔ 𝑦 ∈ ((𝐹𝐴) ∖ (𝐹𝐵))))
5352eqrdv 2734 1 (Fun 𝐹 → (𝐹 “ (𝐴𝐵)) = ((𝐹𝐴) ∖ (𝐹𝐵)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  wo 845  wal 1539   = wceq 1541  wex 1781  wcel 2106  ∃*wmo 2536  cdif 3907   class class class wbr 5105  ccnv 5632  cima 5636  Fun wfun 6490
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-clab 2714  df-cleq 2728  df-clel 2814  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-br 5106  df-opab 5168  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-fun 6498
This theorem is referenced by:  imain  6586  resdif  6805  difpreima  7015  domunsncan  9016  phplem2  9152  php3  9156  phplem4OLD  9164  php3OLD  9168  infdifsn  9593  cantnfp1lem3  9616  enfin1ai  10320  fin1a2lem7  10342  symgfixelsi  19217  dprdf1o  19811  frlmlbs  21203  f1lindf  21228  cnclima  22619  iscncl  22620  qtopcld  23064  qtoprest  23068  qtopcmap  23070  mbfimaicc  24995  ismbf3d  25018  i1fd  25045  ballotlemfrc  33126  poimirlem2  36080  poimirlem4  36082  poimirlem6  36084  poimirlem7  36085  poimirlem9  36087  poimirlem11  36089  poimirlem12  36090  poimirlem13  36091  poimirlem14  36092  poimirlem16  36094  poimirlem19  36097  poimirlem23  36101
  Copyright terms: Public domain W3C validator