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

Theorem suppimacnv 8198
Description: Support sets of functions expressed by inverse images. (Contributed by AV, 31-Mar-2019.) (Revised by AV, 7-Apr-2019.)
Assertion
Ref Expression
suppimacnv ((𝑅𝑉𝑍𝑊) → (𝑅 supp 𝑍) = (𝑅 “ (V ∖ {𝑍})))

Proof of Theorem suppimacnv
Dummy variables 𝑥 𝑦 𝑠 𝑡 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 breq2 5152 . . . . . . . 8 (𝑡 = 𝑠 → (𝑥𝑅𝑡𝑥𝑅𝑠))
21cbvexvw 2034 . . . . . . 7 (∃𝑡 𝑥𝑅𝑡 ↔ ∃𝑠 𝑥𝑅𝑠)
3 breq2 5152 . . . . . . . . . . . . . 14 (𝑠 = 𝑍 → (𝑥𝑅𝑠𝑥𝑅𝑍))
43anbi1d 631 . . . . . . . . . . . . 13 (𝑠 = 𝑍 → ((𝑥𝑅𝑠 ∧ (𝑥𝑅𝑡𝑡𝑍)) ↔ (𝑥𝑅𝑍 ∧ (𝑥𝑅𝑡𝑡𝑍))))
5 bianir 1058 . . . . . . . . . . . . . . . . . 18 ((𝑡𝑍 ∧ (𝑥𝑅𝑡𝑡𝑍)) → 𝑥𝑅𝑡)
6 vex 3482 . . . . . . . . . . . . . . . . . . . 20 𝑡 ∈ V
7 breq2 5152 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑡 → (𝑥𝑅𝑦𝑥𝑅𝑡))
8 neeq1 3001 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑡 → (𝑦𝑍𝑡𝑍))
97, 8anbi12d 632 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑡 → ((𝑥𝑅𝑦𝑦𝑍) ↔ (𝑥𝑅𝑡𝑡𝑍)))
106, 9spcev 3606 . . . . . . . . . . . . . . . . . . 19 ((𝑥𝑅𝑡𝑡𝑍) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍))
1110ex 412 . . . . . . . . . . . . . . . . . 18 (𝑥𝑅𝑡 → (𝑡𝑍 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
125, 11syl 17 . . . . . . . . . . . . . . . . 17 ((𝑡𝑍 ∧ (𝑥𝑅𝑡𝑡𝑍)) → (𝑡𝑍 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
1312ex 412 . . . . . . . . . . . . . . . 16 (𝑡𝑍 → ((𝑥𝑅𝑡𝑡𝑍) → (𝑡𝑍 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍))))
1413pm2.43a 54 . . . . . . . . . . . . . . 15 (𝑡𝑍 → ((𝑥𝑅𝑡𝑡𝑍) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
1514adantld 490 . . . . . . . . . . . . . 14 (𝑡𝑍 → ((𝑥𝑅𝑍 ∧ (𝑥𝑅𝑡𝑡𝑍)) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
16 nne 2942 . . . . . . . . . . . . . . . 16 𝑡𝑍𝑡 = 𝑍)
17 notbi 319 . . . . . . . . . . . . . . . . . . . 20 ((𝑥𝑅𝑡𝑡𝑍) ↔ (¬ 𝑥𝑅𝑡 ↔ ¬ 𝑡𝑍))
18 bianir 1058 . . . . . . . . . . . . . . . . . . . . . 22 ((¬ 𝑡𝑍 ∧ (¬ 𝑥𝑅𝑡 ↔ ¬ 𝑡𝑍)) → ¬ 𝑥𝑅𝑡)
19 breq2 5152 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑍 = 𝑡 → (𝑥𝑅𝑍𝑥𝑅𝑡))
2019eqcoms 2743 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 = 𝑍 → (𝑥𝑅𝑍𝑥𝑅𝑡))
21 pm2.24 124 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥𝑅𝑡 → (¬ 𝑥𝑅𝑡 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
2220, 21biimtrdi 253 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 = 𝑍 → (𝑥𝑅𝑍 → (¬ 𝑥𝑅𝑡 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍))))
2322com13 88 . . . . . . . . . . . . . . . . . . . . . 22 𝑥𝑅𝑡 → (𝑥𝑅𝑍 → (𝑡 = 𝑍 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍))))
2418, 23syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((¬ 𝑡𝑍 ∧ (¬ 𝑥𝑅𝑡 ↔ ¬ 𝑡𝑍)) → (𝑥𝑅𝑍 → (𝑡 = 𝑍 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍))))
2524ex 412 . . . . . . . . . . . . . . . . . . . 20 𝑡𝑍 → ((¬ 𝑥𝑅𝑡 ↔ ¬ 𝑡𝑍) → (𝑥𝑅𝑍 → (𝑡 = 𝑍 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))))
2617, 25biimtrid 242 . . . . . . . . . . . . . . . . . . 19 𝑡𝑍 → ((𝑥𝑅𝑡𝑡𝑍) → (𝑥𝑅𝑍 → (𝑡 = 𝑍 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))))
2726com13 88 . . . . . . . . . . . . . . . . . 18 (𝑥𝑅𝑍 → ((𝑥𝑅𝑡𝑡𝑍) → (¬ 𝑡𝑍 → (𝑡 = 𝑍 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))))
2827imp 406 . . . . . . . . . . . . . . . . 17 ((𝑥𝑅𝑍 ∧ (𝑥𝑅𝑡𝑡𝑍)) → (¬ 𝑡𝑍 → (𝑡 = 𝑍 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍))))
2928com13 88 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑍 → (¬ 𝑡𝑍 → ((𝑥𝑅𝑍 ∧ (𝑥𝑅𝑡𝑡𝑍)) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍))))
3016, 29sylbi 217 . . . . . . . . . . . . . . 15 𝑡𝑍 → (¬ 𝑡𝑍 → ((𝑥𝑅𝑍 ∧ (𝑥𝑅𝑡𝑡𝑍)) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍))))
3130pm2.43i 52 . . . . . . . . . . . . . 14 𝑡𝑍 → ((𝑥𝑅𝑍 ∧ (𝑥𝑅𝑡𝑡𝑍)) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
3215, 31pm2.61i 182 . . . . . . . . . . . . 13 ((𝑥𝑅𝑍 ∧ (𝑥𝑅𝑡𝑡𝑍)) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍))
334, 32biimtrdi 253 . . . . . . . . . . . 12 (𝑠 = 𝑍 → ((𝑥𝑅𝑠 ∧ (𝑥𝑅𝑡𝑡𝑍)) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
34 vex 3482 . . . . . . . . . . . . . . . 16 𝑠 ∈ V
35 breq2 5152 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑠 → (𝑥𝑅𝑦𝑥𝑅𝑠))
36 neeq1 3001 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑠 → (𝑦𝑍𝑠𝑍))
3735, 36anbi12d 632 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑠 → ((𝑥𝑅𝑦𝑦𝑍) ↔ (𝑥𝑅𝑠𝑠𝑍)))
3834, 37spcev 3606 . . . . . . . . . . . . . . 15 ((𝑥𝑅𝑠𝑠𝑍) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍))
3938ex 412 . . . . . . . . . . . . . 14 (𝑥𝑅𝑠 → (𝑠𝑍 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
4039adantr 480 . . . . . . . . . . . . 13 ((𝑥𝑅𝑠 ∧ (𝑥𝑅𝑡𝑡𝑍)) → (𝑠𝑍 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
4140com12 32 . . . . . . . . . . . 12 (𝑠𝑍 → ((𝑥𝑅𝑠 ∧ (𝑥𝑅𝑡𝑡𝑍)) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
4233, 41pm2.61ine 3023 . . . . . . . . . . 11 ((𝑥𝑅𝑠 ∧ (𝑥𝑅𝑡𝑡𝑍)) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍))
4342expcom 413 . . . . . . . . . 10 ((𝑥𝑅𝑡𝑡𝑍) → (𝑥𝑅𝑠 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
4443exlimiv 1928 . . . . . . . . 9 (∃𝑡(𝑥𝑅𝑡𝑡𝑍) → (𝑥𝑅𝑠 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
4544com12 32 . . . . . . . 8 (𝑥𝑅𝑠 → (∃𝑡(𝑥𝑅𝑡𝑡𝑍) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
4645exlimiv 1928 . . . . . . 7 (∃𝑠 𝑥𝑅𝑠 → (∃𝑡(𝑥𝑅𝑡𝑡𝑍) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
472, 46sylbi 217 . . . . . 6 (∃𝑡 𝑥𝑅𝑡 → (∃𝑡(𝑥𝑅𝑡𝑡𝑍) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
4847imp 406 . . . . 5 ((∃𝑡 𝑥𝑅𝑡 ∧ ∃𝑡(𝑥𝑅𝑡𝑡𝑍)) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍))
4948a1i 11 . . . 4 ((𝑅𝑉𝑍𝑊) → ((∃𝑡 𝑥𝑅𝑡 ∧ ∃𝑡(𝑥𝑅𝑡𝑡𝑍)) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
5049ss2abdv 4076 . . 3 ((𝑅𝑉𝑍𝑊) → {𝑥 ∣ (∃𝑡 𝑥𝑅𝑡 ∧ ∃𝑡(𝑥𝑅𝑡𝑡𝑍))} ⊆ {𝑥 ∣ ∃𝑦(𝑥𝑅𝑦𝑦𝑍)})
51 suppvalbr 8188 . . 3 ((𝑅𝑉𝑍𝑊) → (𝑅 supp 𝑍) = {𝑥 ∣ (∃𝑡 𝑥𝑅𝑡 ∧ ∃𝑡(𝑥𝑅𝑡𝑡𝑍))})
52 cnvimadfsn 8196 . . . 4 (𝑅 “ (V ∖ {𝑍})) = {𝑥 ∣ ∃𝑦(𝑥𝑅𝑦𝑦𝑍)}
5352a1i 11 . . 3 ((𝑅𝑉𝑍𝑊) → (𝑅 “ (V ∖ {𝑍})) = {𝑥 ∣ ∃𝑦(𝑥𝑅𝑦𝑦𝑍)})
5450, 51, 533sstr4d 4043 . 2 ((𝑅𝑉𝑍𝑊) → (𝑅 supp 𝑍) ⊆ (𝑅 “ (V ∖ {𝑍})))
55 suppimacnvss 8197 . 2 ((𝑅𝑉𝑍𝑊) → (𝑅 “ (V ∖ {𝑍})) ⊆ (𝑅 supp 𝑍))
5654, 55eqssd 4013 1 ((𝑅𝑉𝑍𝑊) → (𝑅 supp 𝑍) = (𝑅 “ (V ∖ {𝑍})))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395   = wceq 1537  wex 1776  wcel 2106  {cab 2712  wne 2938  Vcvv 3478  cdif 3960  {csn 4631   class class class wbr 5148  ccnv 5688  cima 5692  (class class class)co 7431   supp csupp 8184
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-sbc 3792  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fv 6571  df-ov 7434  df-oprab 7435  df-mpo 7436  df-supp 8185
This theorem is referenced by:  fsuppeq  8199  fsuppeqg  8200  suppun  8208  mptsuppdifd  8210  suppco  8230  fidmfisupp  9410  fdmfisuppfi  9412  fsuppun  9425  fsuppco  9440  gsumval3a  19936  gsumzf1o  19945  gsumzaddlem  19954  gsumzmhm  19970  gsumzoppg  19977  deg1val  26150  suppun2  32699  suppss3  32742  ffsrn  32747  fpwrelmapffslem  32750  sitgclg  34324  eulerpartlemmf  34357  eulerpartlemgf  34361
  Copyright terms: Public domain W3C validator