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

Theorem suppimacnv 7853
 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 5039 . . . . . . . 8 (𝑡 = 𝑠 → (𝑥𝑅𝑡𝑥𝑅𝑠))
21cbvexvw 2044 . . . . . . 7 (∃𝑡 𝑥𝑅𝑡 ↔ ∃𝑠 𝑥𝑅𝑠)
3 breq2 5039 . . . . . . . . . . . . . 14 (𝑠 = 𝑍 → (𝑥𝑅𝑠𝑥𝑅𝑍))
43anbi1d 632 . . . . . . . . . . . . 13 (𝑠 = 𝑍 → ((𝑥𝑅𝑠 ∧ (𝑥𝑅𝑡𝑡𝑍)) ↔ (𝑥𝑅𝑍 ∧ (𝑥𝑅𝑡𝑡𝑍))))
5 bianir 1054 . . . . . . . . . . . . . . . . . 18 ((𝑡𝑍 ∧ (𝑥𝑅𝑡𝑡𝑍)) → 𝑥𝑅𝑡)
6 vex 3413 . . . . . . . . . . . . . . . . . . . 20 𝑡 ∈ V
7 breq2 5039 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑡 → (𝑥𝑅𝑦𝑥𝑅𝑡))
8 neeq1 3013 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑡 → (𝑦𝑍𝑡𝑍))
97, 8anbi12d 633 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑡 → ((𝑥𝑅𝑦𝑦𝑍) ↔ (𝑥𝑅𝑡𝑡𝑍)))
106, 9spcev 3527 . . . . . . . . . . . . . . . . . . 19 ((𝑥𝑅𝑡𝑡𝑍) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍))
1110ex 416 . . . . . . . . . . . . . . . . . 18 (𝑥𝑅𝑡 → (𝑡𝑍 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
125, 11syl 17 . . . . . . . . . . . . . . . . 17 ((𝑡𝑍 ∧ (𝑥𝑅𝑡𝑡𝑍)) → (𝑡𝑍 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
1312ex 416 . . . . . . . . . . . . . . . 16 (𝑡𝑍 → ((𝑥𝑅𝑡𝑡𝑍) → (𝑡𝑍 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍))))
1413pm2.43a 54 . . . . . . . . . . . . . . 15 (𝑡𝑍 → ((𝑥𝑅𝑡𝑡𝑍) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
1514adantld 494 . . . . . . . . . . . . . 14 (𝑡𝑍 → ((𝑥𝑅𝑍 ∧ (𝑥𝑅𝑡𝑡𝑍)) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
16 nne 2955 . . . . . . . . . . . . . . . 16 𝑡𝑍𝑡 = 𝑍)
17 notbi 322 . . . . . . . . . . . . . . . . . . . 20 ((𝑥𝑅𝑡𝑡𝑍) ↔ (¬ 𝑥𝑅𝑡 ↔ ¬ 𝑡𝑍))
18 bianir 1054 . . . . . . . . . . . . . . . . . . . . . 22 ((¬ 𝑡𝑍 ∧ (¬ 𝑥𝑅𝑡 ↔ ¬ 𝑡𝑍)) → ¬ 𝑥𝑅𝑡)
19 breq2 5039 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑍 = 𝑡 → (𝑥𝑅𝑍𝑥𝑅𝑡))
2019eqcoms 2766 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 = 𝑍 → (𝑥𝑅𝑍𝑥𝑅𝑡))
21 pm2.24 124 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥𝑅𝑡 → (¬ 𝑥𝑅𝑡 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
2220, 21syl6bi 256 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 = 𝑍 → (𝑥𝑅𝑍 → (¬ 𝑥𝑅𝑡 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍))))
2322com13 88 . . . . . . . . . . . . . . . . . . . . . 22 𝑥𝑅𝑡 → (𝑥𝑅𝑍 → (𝑡 = 𝑍 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍))))
2418, 23syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((¬ 𝑡𝑍 ∧ (¬ 𝑥𝑅𝑡 ↔ ¬ 𝑡𝑍)) → (𝑥𝑅𝑍 → (𝑡 = 𝑍 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍))))
2524ex 416 . . . . . . . . . . . . . . . . . . . 20 𝑡𝑍 → ((¬ 𝑥𝑅𝑡 ↔ ¬ 𝑡𝑍) → (𝑥𝑅𝑍 → (𝑡 = 𝑍 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))))
2617, 25syl5bi 245 . . . . . . . . . . . . . . . . . . 19 𝑡𝑍 → ((𝑥𝑅𝑡𝑡𝑍) → (𝑥𝑅𝑍 → (𝑡 = 𝑍 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))))
2726com13 88 . . . . . . . . . . . . . . . . . 18 (𝑥𝑅𝑍 → ((𝑥𝑅𝑡𝑡𝑍) → (¬ 𝑡𝑍 → (𝑡 = 𝑍 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))))
2827imp 410 . . . . . . . . . . . . . . . . 17 ((𝑥𝑅𝑍 ∧ (𝑥𝑅𝑡𝑡𝑍)) → (¬ 𝑡𝑍 → (𝑡 = 𝑍 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍))))
2928com13 88 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑍 → (¬ 𝑡𝑍 → ((𝑥𝑅𝑍 ∧ (𝑥𝑅𝑡𝑡𝑍)) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍))))
3016, 29sylbi 220 . . . . . . . . . . . . . . 15 𝑡𝑍 → (¬ 𝑡𝑍 → ((𝑥𝑅𝑍 ∧ (𝑥𝑅𝑡𝑡𝑍)) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍))))
3130pm2.43i 52 . . . . . . . . . . . . . 14 𝑡𝑍 → ((𝑥𝑅𝑍 ∧ (𝑥𝑅𝑡𝑡𝑍)) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
3215, 31pm2.61i 185 . . . . . . . . . . . . 13 ((𝑥𝑅𝑍 ∧ (𝑥𝑅𝑡𝑡𝑍)) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍))
334, 32syl6bi 256 . . . . . . . . . . . 12 (𝑠 = 𝑍 → ((𝑥𝑅𝑠 ∧ (𝑥𝑅𝑡𝑡𝑍)) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
34 vex 3413 . . . . . . . . . . . . . . . 16 𝑠 ∈ V
35 breq2 5039 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑠 → (𝑥𝑅𝑦𝑥𝑅𝑠))
36 neeq1 3013 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑠 → (𝑦𝑍𝑠𝑍))
3735, 36anbi12d 633 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑠 → ((𝑥𝑅𝑦𝑦𝑍) ↔ (𝑥𝑅𝑠𝑠𝑍)))
3834, 37spcev 3527 . . . . . . . . . . . . . . 15 ((𝑥𝑅𝑠𝑠𝑍) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍))
3938ex 416 . . . . . . . . . . . . . 14 (𝑥𝑅𝑠 → (𝑠𝑍 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
4039adantr 484 . . . . . . . . . . . . 13 ((𝑥𝑅𝑠 ∧ (𝑥𝑅𝑡𝑡𝑍)) → (𝑠𝑍 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
4140com12 32 . . . . . . . . . . . 12 (𝑠𝑍 → ((𝑥𝑅𝑠 ∧ (𝑥𝑅𝑡𝑡𝑍)) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
4233, 41pm2.61ine 3034 . . . . . . . . . . 11 ((𝑥𝑅𝑠 ∧ (𝑥𝑅𝑡𝑡𝑍)) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍))
4342expcom 417 . . . . . . . . . 10 ((𝑥𝑅𝑡𝑡𝑍) → (𝑥𝑅𝑠 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
4443exlimiv 1931 . . . . . . . . 9 (∃𝑡(𝑥𝑅𝑡𝑡𝑍) → (𝑥𝑅𝑠 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
4544com12 32 . . . . . . . 8 (𝑥𝑅𝑠 → (∃𝑡(𝑥𝑅𝑡𝑡𝑍) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
4645exlimiv 1931 . . . . . . 7 (∃𝑠 𝑥𝑅𝑠 → (∃𝑡(𝑥𝑅𝑡𝑡𝑍) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
472, 46sylbi 220 . . . . . 6 (∃𝑡 𝑥𝑅𝑡 → (∃𝑡(𝑥𝑅𝑡𝑡𝑍) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
4847imp 410 . . . . 5 ((∃𝑡 𝑥𝑅𝑡 ∧ ∃𝑡(𝑥𝑅𝑡𝑡𝑍)) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍))
4948a1i 11 . . . 4 ((𝑅𝑉𝑍𝑊) → ((∃𝑡 𝑥𝑅𝑡 ∧ ∃𝑡(𝑥𝑅𝑡𝑡𝑍)) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
5049ss2abdv 3970 . . 3 ((𝑅𝑉𝑍𝑊) → {𝑥 ∣ (∃𝑡 𝑥𝑅𝑡 ∧ ∃𝑡(𝑥𝑅𝑡𝑡𝑍))} ⊆ {𝑥 ∣ ∃𝑦(𝑥𝑅𝑦𝑦𝑍)})
51 suppvalbr 7844 . . 3 ((𝑅𝑉𝑍𝑊) → (𝑅 supp 𝑍) = {𝑥 ∣ (∃𝑡 𝑥𝑅𝑡 ∧ ∃𝑡(𝑥𝑅𝑡𝑡𝑍))})
52 cnvimadfsn 7851 . . . 4 (𝑅 “ (V ∖ {𝑍})) = {𝑥 ∣ ∃𝑦(𝑥𝑅𝑦𝑦𝑍)}
5352a1i 11 . . 3 ((𝑅𝑉𝑍𝑊) → (𝑅 “ (V ∖ {𝑍})) = {𝑥 ∣ ∃𝑦(𝑥𝑅𝑦𝑦𝑍)})
5450, 51, 533sstr4d 3941 . 2 ((𝑅𝑉𝑍𝑊) → (𝑅 supp 𝑍) ⊆ (𝑅 “ (V ∖ {𝑍})))
55 suppimacnvss 7852 . 2 ((𝑅𝑉𝑍𝑊) → (𝑅 “ (V ∖ {𝑍})) ⊆ (𝑅 supp 𝑍))
5654, 55eqssd 3911 1 ((𝑅𝑉𝑍𝑊) → (𝑅 supp 𝑍) = (𝑅 “ (V ∖ {𝑍})))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2111  {cab 2735   ≠ wne 2951  Vcvv 3409   ∖ cdif 3857  {csn 4525   class class class wbr 5035  ◡ccnv 5526   “ cima 5530  (class class class)co 7155   supp csupp 7840 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 2729  ax-sep 5172  ax-nul 5179  ax-pr 5301  ax-un 7464 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-rab 3079  df-v 3411  df-sbc 3699  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-nul 4228  df-if 4424  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-br 5036  df-opab 5098  df-id 5433  df-xp 5533  df-rel 5534  df-cnv 5535  df-co 5536  df-dm 5537  df-rn 5538  df-res 5539  df-ima 5540  df-iota 6298  df-fun 6341  df-fv 6347  df-ov 7158  df-oprab 7159  df-mpo 7160  df-supp 7841 This theorem is referenced by:  frnsuppeq  7854  frnsuppeqg  7855  suppun  7863  mptsuppdifd  7865  suppco  7885  supp0cosupp0OLD  7888  imacosuppOLD  7890  fdmfisuppfi  8880  fsuppun  8890  fsuppco  8904  gsumval3a  19096  gsumzf1o  19105  gsumzaddlem  19114  gsumzmhm  19130  gsumzoppg  19137  deg1val  24801  suppss3  30587  ffsrn  30592  fpwrelmapffslem  30595  sitgclg  31832  eulerpartlemmf  31865  eulerpartlemgf  31869  fidmfisupp  42226
 Copyright terms: Public domain W3C validator