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

Theorem imadif 6631
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 673 . . . . . . . 8 (((𝑥𝐴 ∧ ¬ 𝑥𝐵) ∧ 𝑥𝐹𝑦) ↔ ((𝑥𝐴𝑥𝐹𝑦) ∧ (¬ 𝑥𝐵𝑥𝐹𝑦)))
21exbii 1848 . . . . . . 7 (∃𝑥((𝑥𝐴 ∧ ¬ 𝑥𝐵) ∧ 𝑥𝐹𝑦) ↔ ∃𝑥((𝑥𝐴𝑥𝐹𝑦) ∧ (¬ 𝑥𝐵𝑥𝐹𝑦)))
3 19.40 1887 . . . . . . 7 (∃𝑥((𝑥𝐴𝑥𝐹𝑦) ∧ (¬ 𝑥𝐵𝑥𝐹𝑦)) → (∃𝑥(𝑥𝐴𝑥𝐹𝑦) ∧ ∃𝑥𝑥𝐵𝑥𝐹𝑦)))
42, 3sylbi 216 . . . . . 6 (∃𝑥((𝑥𝐴 ∧ ¬ 𝑥𝐵) ∧ 𝑥𝐹𝑦) → (∃𝑥(𝑥𝐴𝑥𝐹𝑦) ∧ ∃𝑥𝑥𝐵𝑥𝐹𝑦)))
5 nfv 1915 . . . . . . . . . . 11 𝑥Fun 𝐹
6 nfe1 2145 . . . . . . . . . . 11 𝑥𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥𝐵)
75, 6nfan 1900 . . . . . . . . . 10 𝑥(Fun 𝐹 ∧ ∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥𝐵))
8 funmo 6562 . . . . . . . . . . . . . 14 (Fun 𝐹 → ∃*𝑥 𝑦𝐹𝑥)
9 vex 3476 . . . . . . . . . . . . . . . 16 𝑦 ∈ V
10 vex 3476 . . . . . . . . . . . . . . . 16 𝑥 ∈ V
119, 10brcnv 5881 . . . . . . . . . . . . . . 15 (𝑦𝐹𝑥𝑥𝐹𝑦)
1211mobii 2540 . . . . . . . . . . . . . 14 (∃*𝑥 𝑦𝐹𝑥 ↔ ∃*𝑥 𝑥𝐹𝑦)
138, 12sylib 217 . . . . . . . . . . . . 13 (Fun 𝐹 → ∃*𝑥 𝑥𝐹𝑦)
14 mopick 2619 . . . . . . . . . . . . 13 ((∃*𝑥 𝑥𝐹𝑦 ∧ ∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥𝐵)) → (𝑥𝐹𝑦 → ¬ 𝑥𝐵))
1513, 14sylan 578 . . . . . . . . . . . 12 ((Fun 𝐹 ∧ ∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥𝐵)) → (𝑥𝐹𝑦 → ¬ 𝑥𝐵))
1615con2d 134 . . . . . . . . . . 11 ((Fun 𝐹 ∧ ∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥𝐵)) → (𝑥𝐵 → ¬ 𝑥𝐹𝑦))
17 imnan 398 . . . . . . . . . . 11 ((𝑥𝐵 → ¬ 𝑥𝐹𝑦) ↔ ¬ (𝑥𝐵𝑥𝐹𝑦))
1816, 17sylib 217 . . . . . . . . . 10 ((Fun 𝐹 ∧ ∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥𝐵)) → ¬ (𝑥𝐵𝑥𝐹𝑦))
197, 18alrimi 2204 . . . . . . . . 9 ((Fun 𝐹 ∧ ∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥𝐵)) → ∀𝑥 ¬ (𝑥𝐵𝑥𝐹𝑦))
2019ex 411 . . . . . . . 8 (Fun 𝐹 → (∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥𝐵) → ∀𝑥 ¬ (𝑥𝐵𝑥𝐹𝑦)))
21 exancom 1862 . . . . . . . 8 (∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥𝐵) ↔ ∃𝑥𝑥𝐵𝑥𝐹𝑦))
22 alnex 1781 . . . . . . . 8 (∀𝑥 ¬ (𝑥𝐵𝑥𝐹𝑦) ↔ ¬ ∃𝑥(𝑥𝐵𝑥𝐹𝑦))
2320, 21, 223imtr3g 294 . . . . . . 7 (Fun 𝐹 → (∃𝑥𝑥𝐵𝑥𝐹𝑦) → ¬ ∃𝑥(𝑥𝐵𝑥𝐹𝑦)))
2423anim2d 610 . . . . . 6 (Fun 𝐹 → ((∃𝑥(𝑥𝐴𝑥𝐹𝑦) ∧ ∃𝑥𝑥𝐵𝑥𝐹𝑦)) → (∃𝑥(𝑥𝐴𝑥𝐹𝑦) ∧ ¬ ∃𝑥(𝑥𝐵𝑥𝐹𝑦))))
254, 24syl5 34 . . . . 5 (Fun 𝐹 → (∃𝑥((𝑥𝐴 ∧ ¬ 𝑥𝐵) ∧ 𝑥𝐹𝑦) → (∃𝑥(𝑥𝐴𝑥𝐹𝑦) ∧ ¬ ∃𝑥(𝑥𝐵𝑥𝐹𝑦))))
26 19.29r 1875 . . . . . . 7 ((∃𝑥(𝑥𝐴𝑥𝐹𝑦) ∧ ∀𝑥 ¬ (𝑥𝐵𝑥𝐹𝑦)) → ∃𝑥((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ (𝑥𝐵𝑥𝐹𝑦)))
2722, 26sylan2br 593 . . . . . 6 ((∃𝑥(𝑥𝐴𝑥𝐹𝑦) ∧ ¬ ∃𝑥(𝑥𝐵𝑥𝐹𝑦)) → ∃𝑥((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ (𝑥𝐵𝑥𝐹𝑦)))
28 andi 1004 . . . . . . . 8 (((𝑥𝐴𝑥𝐹𝑦) ∧ (¬ 𝑥𝐵 ∨ ¬ 𝑥𝐹𝑦)) ↔ (((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ 𝑥𝐵) ∨ ((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ 𝑥𝐹𝑦)))
29 ianor 978 . . . . . . . . 9 (¬ (𝑥𝐵𝑥𝐹𝑦) ↔ (¬ 𝑥𝐵 ∨ ¬ 𝑥𝐹𝑦))
3029anbi2i 621 . . . . . . . 8 (((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ (𝑥𝐵𝑥𝐹𝑦)) ↔ ((𝑥𝐴𝑥𝐹𝑦) ∧ (¬ 𝑥𝐵 ∨ ¬ 𝑥𝐹𝑦)))
31 an32 642 . . . . . . . . 9 (((𝑥𝐴 ∧ ¬ 𝑥𝐵) ∧ 𝑥𝐹𝑦) ↔ ((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ 𝑥𝐵))
32 pm3.24 401 . . . . . . . . . . . 12 ¬ (𝑥𝐹𝑦 ∧ ¬ 𝑥𝐹𝑦)
3332intnan 485 . . . . . . . . . . 11 ¬ (𝑥𝐴 ∧ (𝑥𝐹𝑦 ∧ ¬ 𝑥𝐹𝑦))
34 anass 467 . . . . . . . . . . 11 (((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ 𝑥𝐹𝑦) ↔ (𝑥𝐴 ∧ (𝑥𝐹𝑦 ∧ ¬ 𝑥𝐹𝑦)))
3533, 34mtbir 322 . . . . . . . . . 10 ¬ ((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ 𝑥𝐹𝑦)
3635biorfi 935 . . . . . . . . 9 (((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ 𝑥𝐵) ↔ (((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ 𝑥𝐵) ∨ ((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ 𝑥𝐹𝑦)))
3731, 36bitri 274 . . . . . . . 8 (((𝑥𝐴 ∧ ¬ 𝑥𝐵) ∧ 𝑥𝐹𝑦) ↔ (((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ 𝑥𝐵) ∨ ((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ 𝑥𝐹𝑦)))
3828, 30, 373bitr4i 302 . . . . . . 7 (((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ (𝑥𝐵𝑥𝐹𝑦)) ↔ ((𝑥𝐴 ∧ ¬ 𝑥𝐵) ∧ 𝑥𝐹𝑦))
3938exbii 1848 . . . . . 6 (∃𝑥((𝑥𝐴𝑥𝐹𝑦) ∧ ¬ (𝑥𝐵𝑥𝐹𝑦)) ↔ ∃𝑥((𝑥𝐴 ∧ ¬ 𝑥𝐵) ∧ 𝑥𝐹𝑦))
4027, 39sylib 217 . . . . 5 ((∃𝑥(𝑥𝐴𝑥𝐹𝑦) ∧ ¬ ∃𝑥(𝑥𝐵𝑥𝐹𝑦)) → ∃𝑥((𝑥𝐴 ∧ ¬ 𝑥𝐵) ∧ 𝑥𝐹𝑦))
4125, 40impbid1 224 . . . 4 (Fun 𝐹 → (∃𝑥((𝑥𝐴 ∧ ¬ 𝑥𝐵) ∧ 𝑥𝐹𝑦) ↔ (∃𝑥(𝑥𝐴𝑥𝐹𝑦) ∧ ¬ ∃𝑥(𝑥𝐵𝑥𝐹𝑦))))
42 eldif 3957 . . . . . 6 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐵))
4342anbi1i 622 . . . . 5 ((𝑥 ∈ (𝐴𝐵) ∧ 𝑥𝐹𝑦) ↔ ((𝑥𝐴 ∧ ¬ 𝑥𝐵) ∧ 𝑥𝐹𝑦))
4443exbii 1848 . . . 4 (∃𝑥(𝑥 ∈ (𝐴𝐵) ∧ 𝑥𝐹𝑦) ↔ ∃𝑥((𝑥𝐴 ∧ ¬ 𝑥𝐵) ∧ 𝑥𝐹𝑦))
459elima2 6064 . . . . 5 (𝑦 ∈ (𝐹𝐴) ↔ ∃𝑥(𝑥𝐴𝑥𝐹𝑦))
469elima2 6064 . . . . . 6 (𝑦 ∈ (𝐹𝐵) ↔ ∃𝑥(𝑥𝐵𝑥𝐹𝑦))
4746notbii 319 . . . . 5 𝑦 ∈ (𝐹𝐵) ↔ ¬ ∃𝑥(𝑥𝐵𝑥𝐹𝑦))
4845, 47anbi12i 625 . . . 4 ((𝑦 ∈ (𝐹𝐴) ∧ ¬ 𝑦 ∈ (𝐹𝐵)) ↔ (∃𝑥(𝑥𝐴𝑥𝐹𝑦) ∧ ¬ ∃𝑥(𝑥𝐵𝑥𝐹𝑦)))
4941, 44, 483bitr4g 313 . . 3 (Fun 𝐹 → (∃𝑥(𝑥 ∈ (𝐴𝐵) ∧ 𝑥𝐹𝑦) ↔ (𝑦 ∈ (𝐹𝐴) ∧ ¬ 𝑦 ∈ (𝐹𝐵))))
509elima2 6064 . . 3 (𝑦 ∈ (𝐹 “ (𝐴𝐵)) ↔ ∃𝑥(𝑥 ∈ (𝐴𝐵) ∧ 𝑥𝐹𝑦))
51 eldif 3957 . . 3 (𝑦 ∈ ((𝐹𝐴) ∖ (𝐹𝐵)) ↔ (𝑦 ∈ (𝐹𝐴) ∧ ¬ 𝑦 ∈ (𝐹𝐵)))
5249, 50, 513bitr4g 313 . 2 (Fun 𝐹 → (𝑦 ∈ (𝐹 “ (𝐴𝐵)) ↔ 𝑦 ∈ ((𝐹𝐴) ∖ (𝐹𝐵))))
5352eqrdv 2728 1 (Fun 𝐹 → (𝐹 “ (𝐴𝐵)) = ((𝐹𝐴) ∖ (𝐹𝐵)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 394  wo 843  wal 1537   = wceq 1539  wex 1779  wcel 2104  ∃*wmo 2530  cdif 3944   class class class wbr 5147  ccnv 5674  cima 5678  Fun wfun 6536
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-clab 2708  df-cleq 2722  df-clel 2808  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-opab 5210  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-fun 6544
This theorem is referenced by:  imain  6632  resdif  6853  difpreima  7065  domunsncan  9074  phplem2  9210  php3  9214  phplem4OLD  9222  php3OLD  9226  infdifsn  9654  cantnfp1lem3  9677  enfin1ai  10381  fin1a2lem7  10403  symgfixelsi  19344  dprdf1o  19943  frlmlbs  21571  f1lindf  21596  cnclima  22992  iscncl  22993  qtopcld  23437  qtoprest  23441  qtopcmap  23443  mbfimaicc  25380  ismbf3d  25403  i1fd  25430  ballotlemfrc  33823  poimirlem2  36793  poimirlem4  36795  poimirlem6  36797  poimirlem7  36798  poimirlem9  36800  poimirlem11  36802  poimirlem12  36803  poimirlem13  36804  poimirlem14  36805  poimirlem16  36807  poimirlem19  36810  poimirlem23  36814
  Copyright terms: Public domain W3C validator