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

Theorem suppimacnv 7512
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 4815 . . . . . . . 8 (𝑡 = 𝑠 → (𝑥𝑅𝑡𝑥𝑅𝑠))
21cbvexvw 2137 . . . . . . 7 (∃𝑡 𝑥𝑅𝑡 ↔ ∃𝑠 𝑥𝑅𝑠)
3 breq2 4815 . . . . . . . . . . . . . 14 (𝑠 = 𝑍 → (𝑥𝑅𝑠𝑥𝑅𝑍))
43anbi1d 623 . . . . . . . . . . . . 13 (𝑠 = 𝑍 → ((𝑥𝑅𝑠 ∧ (𝑥𝑅𝑡𝑡𝑍)) ↔ (𝑥𝑅𝑍 ∧ (𝑥𝑅𝑡𝑡𝑍))))
5 bianir 1081 . . . . . . . . . . . . . . . . . 18 ((𝑡𝑍 ∧ (𝑥𝑅𝑡𝑡𝑍)) → 𝑥𝑅𝑡)
6 vex 3353 . . . . . . . . . . . . . . . . . . . 20 𝑡 ∈ V
7 breq2 4815 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑡 → (𝑥𝑅𝑦𝑥𝑅𝑡))
8 neeq1 2999 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑡 → (𝑦𝑍𝑡𝑍))
97, 8anbi12d 624 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑡 → ((𝑥𝑅𝑦𝑦𝑍) ↔ (𝑥𝑅𝑡𝑡𝑍)))
106, 9spcev 3453 . . . . . . . . . . . . . . . . . . 19 ((𝑥𝑅𝑡𝑡𝑍) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍))
1110ex 401 . . . . . . . . . . . . . . . . . 18 (𝑥𝑅𝑡 → (𝑡𝑍 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
125, 11syl 17 . . . . . . . . . . . . . . . . 17 ((𝑡𝑍 ∧ (𝑥𝑅𝑡𝑡𝑍)) → (𝑡𝑍 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
1312ex 401 . . . . . . . . . . . . . . . 16 (𝑡𝑍 → ((𝑥𝑅𝑡𝑡𝑍) → (𝑡𝑍 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍))))
1413pm2.43a 54 . . . . . . . . . . . . . . 15 (𝑡𝑍 → ((𝑥𝑅𝑡𝑡𝑍) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
1514adantld 484 . . . . . . . . . . . . . 14 (𝑡𝑍 → ((𝑥𝑅𝑍 ∧ (𝑥𝑅𝑡𝑡𝑍)) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
16 nne 2941 . . . . . . . . . . . . . . . 16 𝑡𝑍𝑡 = 𝑍)
17 notbi 310 . . . . . . . . . . . . . . . . . . . 20 ((𝑥𝑅𝑡𝑡𝑍) ↔ (¬ 𝑥𝑅𝑡 ↔ ¬ 𝑡𝑍))
18 bianir 1081 . . . . . . . . . . . . . . . . . . . . . 22 ((¬ 𝑡𝑍 ∧ (¬ 𝑥𝑅𝑡 ↔ ¬ 𝑡𝑍)) → ¬ 𝑥𝑅𝑡)
19 breq2 4815 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑍 = 𝑡 → (𝑥𝑅𝑍𝑥𝑅𝑡))
2019eqcoms 2773 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 = 𝑍 → (𝑥𝑅𝑍𝑥𝑅𝑡))
21 pm2.24 122 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥𝑅𝑡 → (¬ 𝑥𝑅𝑡 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
2220, 21syl6bi 244 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 = 𝑍 → (𝑥𝑅𝑍 → (¬ 𝑥𝑅𝑡 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍))))
2322com13 88 . . . . . . . . . . . . . . . . . . . . . 22 𝑥𝑅𝑡 → (𝑥𝑅𝑍 → (𝑡 = 𝑍 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍))))
2418, 23syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((¬ 𝑡𝑍 ∧ (¬ 𝑥𝑅𝑡 ↔ ¬ 𝑡𝑍)) → (𝑥𝑅𝑍 → (𝑡 = 𝑍 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍))))
2524ex 401 . . . . . . . . . . . . . . . . . . . 20 𝑡𝑍 → ((¬ 𝑥𝑅𝑡 ↔ ¬ 𝑡𝑍) → (𝑥𝑅𝑍 → (𝑡 = 𝑍 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))))
2617, 25syl5bi 233 . . . . . . . . . . . . . . . . . . 19 𝑡𝑍 → ((𝑥𝑅𝑡𝑡𝑍) → (𝑥𝑅𝑍 → (𝑡 = 𝑍 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))))
2726com13 88 . . . . . . . . . . . . . . . . . 18 (𝑥𝑅𝑍 → ((𝑥𝑅𝑡𝑡𝑍) → (¬ 𝑡𝑍 → (𝑡 = 𝑍 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))))
2827imp 395 . . . . . . . . . . . . . . . . 17 ((𝑥𝑅𝑍 ∧ (𝑥𝑅𝑡𝑡𝑍)) → (¬ 𝑡𝑍 → (𝑡 = 𝑍 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍))))
2928com13 88 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑍 → (¬ 𝑡𝑍 → ((𝑥𝑅𝑍 ∧ (𝑥𝑅𝑡𝑡𝑍)) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍))))
3016, 29sylbi 208 . . . . . . . . . . . . . . 15 𝑡𝑍 → (¬ 𝑡𝑍 → ((𝑥𝑅𝑍 ∧ (𝑥𝑅𝑡𝑡𝑍)) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍))))
3130pm2.43i 52 . . . . . . . . . . . . . 14 𝑡𝑍 → ((𝑥𝑅𝑍 ∧ (𝑥𝑅𝑡𝑡𝑍)) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
3215, 31pm2.61i 176 . . . . . . . . . . . . 13 ((𝑥𝑅𝑍 ∧ (𝑥𝑅𝑡𝑡𝑍)) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍))
334, 32syl6bi 244 . . . . . . . . . . . 12 (𝑠 = 𝑍 → ((𝑥𝑅𝑠 ∧ (𝑥𝑅𝑡𝑡𝑍)) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
34 vex 3353 . . . . . . . . . . . . . . . 16 𝑠 ∈ V
35 breq2 4815 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑠 → (𝑥𝑅𝑦𝑥𝑅𝑠))
36 neeq1 2999 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑠 → (𝑦𝑍𝑠𝑍))
3735, 36anbi12d 624 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑠 → ((𝑥𝑅𝑦𝑦𝑍) ↔ (𝑥𝑅𝑠𝑠𝑍)))
3834, 37spcev 3453 . . . . . . . . . . . . . . 15 ((𝑥𝑅𝑠𝑠𝑍) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍))
3938ex 401 . . . . . . . . . . . . . 14 (𝑥𝑅𝑠 → (𝑠𝑍 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
4039adantr 472 . . . . . . . . . . . . 13 ((𝑥𝑅𝑠 ∧ (𝑥𝑅𝑡𝑡𝑍)) → (𝑠𝑍 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
4140com12 32 . . . . . . . . . . . 12 (𝑠𝑍 → ((𝑥𝑅𝑠 ∧ (𝑥𝑅𝑡𝑡𝑍)) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
4233, 41pm2.61ine 3020 . . . . . . . . . . 11 ((𝑥𝑅𝑠 ∧ (𝑥𝑅𝑡𝑡𝑍)) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍))
4342expcom 402 . . . . . . . . . 10 ((𝑥𝑅𝑡𝑡𝑍) → (𝑥𝑅𝑠 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
4443exlimiv 2025 . . . . . . . . 9 (∃𝑡(𝑥𝑅𝑡𝑡𝑍) → (𝑥𝑅𝑠 → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
4544com12 32 . . . . . . . 8 (𝑥𝑅𝑠 → (∃𝑡(𝑥𝑅𝑡𝑡𝑍) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
4645exlimiv 2025 . . . . . . 7 (∃𝑠 𝑥𝑅𝑠 → (∃𝑡(𝑥𝑅𝑡𝑡𝑍) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
472, 46sylbi 208 . . . . . 6 (∃𝑡 𝑥𝑅𝑡 → (∃𝑡(𝑥𝑅𝑡𝑡𝑍) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
4847imp 395 . . . . 5 ((∃𝑡 𝑥𝑅𝑡 ∧ ∃𝑡(𝑥𝑅𝑡𝑡𝑍)) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍))
4948a1i 11 . . . 4 ((𝑅𝑉𝑍𝑊) → ((∃𝑡 𝑥𝑅𝑡 ∧ ∃𝑡(𝑥𝑅𝑡𝑡𝑍)) → ∃𝑦(𝑥𝑅𝑦𝑦𝑍)))
5049ss2abdv 3837 . . 3 ((𝑅𝑉𝑍𝑊) → {𝑥 ∣ (∃𝑡 𝑥𝑅𝑡 ∧ ∃𝑡(𝑥𝑅𝑡𝑡𝑍))} ⊆ {𝑥 ∣ ∃𝑦(𝑥𝑅𝑦𝑦𝑍)})
51 suppvalbr 7505 . . 3 ((𝑅𝑉𝑍𝑊) → (𝑅 supp 𝑍) = {𝑥 ∣ (∃𝑡 𝑥𝑅𝑡 ∧ ∃𝑡(𝑥𝑅𝑡𝑡𝑍))})
52 cnvimadfsn 7510 . . . 4 (𝑅 “ (V ∖ {𝑍})) = {𝑥 ∣ ∃𝑦(𝑥𝑅𝑦𝑦𝑍)}
5352a1i 11 . . 3 ((𝑅𝑉𝑍𝑊) → (𝑅 “ (V ∖ {𝑍})) = {𝑥 ∣ ∃𝑦(𝑥𝑅𝑦𝑦𝑍)})
5450, 51, 533sstr4d 3810 . 2 ((𝑅𝑉𝑍𝑊) → (𝑅 supp 𝑍) ⊆ (𝑅 “ (V ∖ {𝑍})))
55 suppimacnvss 7511 . 2 ((𝑅𝑉𝑍𝑊) → (𝑅 “ (V ∖ {𝑍})) ⊆ (𝑅 supp 𝑍))
5654, 55eqssd 3780 1 ((𝑅𝑉𝑍𝑊) → (𝑅 supp 𝑍) = (𝑅 “ (V ∖ {𝑍})))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384   = wceq 1652  wex 1874  wcel 2155  {cab 2751  wne 2937  Vcvv 3350  cdif 3731  {csn 4336   class class class wbr 4811  ccnv 5278  cima 5282  (class class class)co 6846   supp csupp 7501
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4943  ax-nul 4951  ax-pr 5064  ax-un 7151
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-rab 3064  df-v 3352  df-sbc 3599  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-nul 4082  df-if 4246  df-sn 4337  df-pr 4339  df-op 4343  df-uni 4597  df-br 4812  df-opab 4874  df-id 5187  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-iota 6033  df-fun 6072  df-fv 6078  df-ov 6849  df-oprab 6850  df-mpt2 6851  df-supp 7502
This theorem is referenced by:  frnsuppeq  7513  suppun  7521  mptsuppdifd  7523  supp0cosupp0  7541  imacosupp  7542  fdmfisuppfi  8495  fsuppun  8505  fsuppco  8518  gsumval3a  18584  gsumzf1o  18593  gsumzaddlem  18601  gsumzmhm  18617  gsumzoppg  18624  deg1val  24161  suppss3  29972  ffsrn  29974  fpwrelmapffslem  29977  sitgclg  30872  eulerpartlemmf  30905  eulerpartlemgf  30909  fidmfisupp  40060
  Copyright terms: Public domain W3C validator