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

Theorem suppimacnv 8105
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 5109 . . . . . . . 8 (𝑡 = 𝑠 → (𝑥𝑅𝑡𝑥𝑅𝑠))
21cbvexvw 2040 . . . . . . 7 (∃𝑡 𝑥𝑅𝑡 ↔ ∃𝑠 𝑥𝑅𝑠)
3 breq2 5109 . . . . . . . . . . . . . 14 (𝑠 = 𝑍 → (𝑥𝑅𝑠𝑥𝑅𝑍))
43anbi1d 630 . . . . . . . . . . . . 13 (𝑠 = 𝑍 → ((𝑥𝑅𝑠 ∧ (𝑥𝑅𝑡𝑡𝑍)) ↔ (𝑥𝑅𝑍 ∧ (𝑥𝑅𝑡𝑡𝑍))))
5 bianir 1057 . . . . . . . . . . . . . . . . . 18 ((𝑡𝑍 ∧ (𝑥𝑅𝑡𝑡𝑍)) → 𝑥𝑅𝑡)
6 vex 3449 . . . . . . . . . . . . . . . . . . . 20 𝑡 ∈ V
7 breq2 5109 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑡 → (𝑥𝑅𝑦𝑥𝑅𝑡))
8 neeq1 3006 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑡 → (𝑦𝑍𝑡𝑍))
97, 8anbi12d 631 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑡 → ((𝑥𝑅𝑦𝑦𝑍) ↔ (𝑥𝑅𝑡𝑡𝑍)))
106, 9spcev 3565 . . . . . . . . . . . . . . . . . . 19 ((𝑥𝑅𝑡𝑡𝑍) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍))
1110ex 413 . . . . . . . . . . . . . . . . . 18 (𝑥𝑅𝑡 → (𝑡𝑍 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
125, 11syl 17 . . . . . . . . . . . . . . . . 17 ((𝑡𝑍 ∧ (𝑥𝑅𝑡𝑡𝑍)) → (𝑡𝑍 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
1312ex 413 . . . . . . . . . . . . . . . 16 (𝑡𝑍 → ((𝑥𝑅𝑡𝑡𝑍) → (𝑡𝑍 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍))))
1413pm2.43a 54 . . . . . . . . . . . . . . 15 (𝑡𝑍 → ((𝑥𝑅𝑡𝑡𝑍) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
1514adantld 491 . . . . . . . . . . . . . 14 (𝑡𝑍 → ((𝑥𝑅𝑍 ∧ (𝑥𝑅𝑡𝑡𝑍)) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
16 nne 2947 . . . . . . . . . . . . . . . 16 𝑡𝑍𝑡 = 𝑍)
17 notbi 318 . . . . . . . . . . . . . . . . . . . 20 ((𝑥𝑅𝑡𝑡𝑍) ↔ (¬ 𝑥𝑅𝑡 ↔ ¬ 𝑡𝑍))
18 bianir 1057 . . . . . . . . . . . . . . . . . . . . . 22 ((¬ 𝑡𝑍 ∧ (¬ 𝑥𝑅𝑡 ↔ ¬ 𝑡𝑍)) → ¬ 𝑥𝑅𝑡)
19 breq2 5109 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑍 = 𝑡 → (𝑥𝑅𝑍𝑥𝑅𝑡))
2019eqcoms 2744 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 = 𝑍 → (𝑥𝑅𝑍𝑥𝑅𝑡))
21 pm2.24 124 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥𝑅𝑡 → (¬ 𝑥𝑅𝑡 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
2220, 21syl6bi 252 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 = 𝑍 → (𝑥𝑅𝑍 → (¬ 𝑥𝑅𝑡 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍))))
2322com13 88 . . . . . . . . . . . . . . . . . . . . . 22 𝑥𝑅𝑡 → (𝑥𝑅𝑍 → (𝑡 = 𝑍 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍))))
2418, 23syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((¬ 𝑡𝑍 ∧ (¬ 𝑥𝑅𝑡 ↔ ¬ 𝑡𝑍)) → (𝑥𝑅𝑍 → (𝑡 = 𝑍 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍))))
2524ex 413 . . . . . . . . . . . . . . . . . . . 20 𝑡𝑍 → ((¬ 𝑥𝑅𝑡 ↔ ¬ 𝑡𝑍) → (𝑥𝑅𝑍 → (𝑡 = 𝑍 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))))
2617, 25biimtrid 241 . . . . . . . . . . . . . . . . . . 19 𝑡𝑍 → ((𝑥𝑅𝑡𝑡𝑍) → (𝑥𝑅𝑍 → (𝑡 = 𝑍 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))))
2726com13 88 . . . . . . . . . . . . . . . . . 18 (𝑥𝑅𝑍 → ((𝑥𝑅𝑡𝑡𝑍) → (¬ 𝑡𝑍 → (𝑡 = 𝑍 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))))
2827imp 407 . . . . . . . . . . . . . . . . 17 ((𝑥𝑅𝑍 ∧ (𝑥𝑅𝑡𝑡𝑍)) → (¬ 𝑡𝑍 → (𝑡 = 𝑍 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍))))
2928com13 88 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑍 → (¬ 𝑡𝑍 → ((𝑥𝑅𝑍 ∧ (𝑥𝑅𝑡𝑡𝑍)) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍))))
3016, 29sylbi 216 . . . . . . . . . . . . . . 15 𝑡𝑍 → (¬ 𝑡𝑍 → ((𝑥𝑅𝑍 ∧ (𝑥𝑅𝑡𝑡𝑍)) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍))))
3130pm2.43i 52 . . . . . . . . . . . . . 14 𝑡𝑍 → ((𝑥𝑅𝑍 ∧ (𝑥𝑅𝑡𝑡𝑍)) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
3215, 31pm2.61i 182 . . . . . . . . . . . . 13 ((𝑥𝑅𝑍 ∧ (𝑥𝑅𝑡𝑡𝑍)) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍))
334, 32syl6bi 252 . . . . . . . . . . . 12 (𝑠 = 𝑍 → ((𝑥𝑅𝑠 ∧ (𝑥𝑅𝑡𝑡𝑍)) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
34 vex 3449 . . . . . . . . . . . . . . . 16 𝑠 ∈ V
35 breq2 5109 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑠 → (𝑥𝑅𝑦𝑥𝑅𝑠))
36 neeq1 3006 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑠 → (𝑦𝑍𝑠𝑍))
3735, 36anbi12d 631 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑠 → ((𝑥𝑅𝑦𝑦𝑍) ↔ (𝑥𝑅𝑠𝑠𝑍)))
3834, 37spcev 3565 . . . . . . . . . . . . . . 15 ((𝑥𝑅𝑠𝑠𝑍) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍))
3938ex 413 . . . . . . . . . . . . . 14 (𝑥𝑅𝑠 → (𝑠𝑍 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
4039adantr 481 . . . . . . . . . . . . 13 ((𝑥𝑅𝑠 ∧ (𝑥𝑅𝑡𝑡𝑍)) → (𝑠𝑍 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
4140com12 32 . . . . . . . . . . . 12 (𝑠𝑍 → ((𝑥𝑅𝑠 ∧ (𝑥𝑅𝑡𝑡𝑍)) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
4233, 41pm2.61ine 3028 . . . . . . . . . . 11 ((𝑥𝑅𝑠 ∧ (𝑥𝑅𝑡𝑡𝑍)) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍))
4342expcom 414 . . . . . . . . . 10 ((𝑥𝑅𝑡𝑡𝑍) → (𝑥𝑅𝑠 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
4443exlimiv 1933 . . . . . . . . 9 (∃𝑡(𝑥𝑅𝑡𝑡𝑍) → (𝑥𝑅𝑠 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
4544com12 32 . . . . . . . 8 (𝑥𝑅𝑠 → (∃𝑡(𝑥𝑅𝑡𝑡𝑍) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
4645exlimiv 1933 . . . . . . 7 (∃𝑠 𝑥𝑅𝑠 → (∃𝑡(𝑥𝑅𝑡𝑡𝑍) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
472, 46sylbi 216 . . . . . 6 (∃𝑡 𝑥𝑅𝑡 → (∃𝑡(𝑥𝑅𝑡𝑡𝑍) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
4847imp 407 . . . . 5 ((∃𝑡 𝑥𝑅𝑡 ∧ ∃𝑡(𝑥𝑅𝑡𝑡𝑍)) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍))
4948a1i 11 . . . 4 ((𝑅𝑉𝑍𝑊) → ((∃𝑡 𝑥𝑅𝑡 ∧ ∃𝑡(𝑥𝑅𝑡𝑡𝑍)) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
5049ss2abdv 4020 . . 3 ((𝑅𝑉𝑍𝑊) → {𝑥 ∣ (∃𝑡 𝑥𝑅𝑡 ∧ ∃𝑡(𝑥𝑅𝑡𝑡𝑍))} ⊆ {𝑥 ∣ ∃𝑦(𝑥𝑅𝑦𝑦𝑍)})
51 suppvalbr 8096 . . 3 ((𝑅𝑉𝑍𝑊) → (𝑅 supp 𝑍) = {𝑥 ∣ (∃𝑡 𝑥𝑅𝑡 ∧ ∃𝑡(𝑥𝑅𝑡𝑡𝑍))})
52 cnvimadfsn 8103 . . . 4 (𝑅 “ (V ∖ {𝑍})) = {𝑥 ∣ ∃𝑦(𝑥𝑅𝑦𝑦𝑍)}
5352a1i 11 . . 3 ((𝑅𝑉𝑍𝑊) → (𝑅 “ (V ∖ {𝑍})) = {𝑥 ∣ ∃𝑦(𝑥𝑅𝑦𝑦𝑍)})
5450, 51, 533sstr4d 3991 . 2 ((𝑅𝑉𝑍𝑊) → (𝑅 supp 𝑍) ⊆ (𝑅 “ (V ∖ {𝑍})))
55 suppimacnvss 8104 . 2 ((𝑅𝑉𝑍𝑊) → (𝑅 “ (V ∖ {𝑍})) ⊆ (𝑅 supp 𝑍))
5654, 55eqssd 3961 1 ((𝑅𝑉𝑍𝑊) → (𝑅 supp 𝑍) = (𝑅 “ (V ∖ {𝑍})))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396   = wceq 1541  wex 1781  wcel 2106  {cab 2713  wne 2943  Vcvv 3445  cdif 3907  {csn 4586   class class class wbr 5105  ccnv 5632  cima 5636  (class class class)co 7357   supp csupp 8092
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-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384  ax-un 7672
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-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-sbc 3740  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-uni 4866  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-iota 6448  df-fun 6498  df-fv 6504  df-ov 7360  df-oprab 7361  df-mpo 7362  df-supp 8093
This theorem is referenced by:  fsuppeq  8106  fsuppeqg  8107  suppun  8115  mptsuppdifd  8117  suppco  8137  fdmfisuppfi  9314  fsuppun  9324  fsuppco  9338  gsumval3a  19680  gsumzf1o  19689  gsumzaddlem  19698  gsumzmhm  19714  gsumzoppg  19721  deg1val  25461  suppss3  31641  ffsrn  31646  fpwrelmapffslem  31649  sitgclg  32942  eulerpartlemmf  32975  eulerpartlemgf  32979  fidmfisupp  43410
  Copyright terms: Public domain W3C validator