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

Theorem funsssuppss 8170
Description: The support of a function which is a subset of another function is a subset of the support of this other function. (Contributed by AV, 27-Jul-2019.)
Assertion
Ref Expression
funsssuppss ((Fun 𝐺𝐹𝐺𝐺𝑉) → (𝐹 supp 𝑍) ⊆ (𝐺 supp 𝑍))

Proof of Theorem funsssuppss
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 funss 6564 . . . . . . . . . 10 (𝐹𝐺 → (Fun 𝐺 → Fun 𝐹))
21impcom 409 . . . . . . . . 9 ((Fun 𝐺𝐹𝐺) → Fun 𝐹)
32funfnd 6576 . . . . . . . 8 ((Fun 𝐺𝐹𝐺) → 𝐹 Fn dom 𝐹)
4 funfn 6575 . . . . . . . . . 10 (Fun 𝐺𝐺 Fn dom 𝐺)
54biimpi 215 . . . . . . . . 9 (Fun 𝐺𝐺 Fn dom 𝐺)
65adantr 482 . . . . . . . 8 ((Fun 𝐺𝐹𝐺) → 𝐺 Fn dom 𝐺)
73, 6jca 513 . . . . . . 7 ((Fun 𝐺𝐹𝐺) → (𝐹 Fn dom 𝐹𝐺 Fn dom 𝐺))
873adant3 1133 . . . . . 6 ((Fun 𝐺𝐹𝐺𝐺𝑉) → (𝐹 Fn dom 𝐹𝐺 Fn dom 𝐺))
98adantr 482 . . . . 5 (((Fun 𝐺𝐹𝐺𝐺𝑉) ∧ 𝑍 ∈ V) → (𝐹 Fn dom 𝐹𝐺 Fn dom 𝐺))
10 dmss 5900 . . . . . . . 8 (𝐹𝐺 → dom 𝐹 ⊆ dom 𝐺)
11103ad2ant2 1135 . . . . . . 7 ((Fun 𝐺𝐹𝐺𝐺𝑉) → dom 𝐹 ⊆ dom 𝐺)
1211adantr 482 . . . . . 6 (((Fun 𝐺𝐹𝐺𝐺𝑉) ∧ 𝑍 ∈ V) → dom 𝐹 ⊆ dom 𝐺)
13 dmexg 7889 . . . . . . . 8 (𝐺𝑉 → dom 𝐺 ∈ V)
14133ad2ant3 1136 . . . . . . 7 ((Fun 𝐺𝐹𝐺𝐺𝑉) → dom 𝐺 ∈ V)
1514adantr 482 . . . . . 6 (((Fun 𝐺𝐹𝐺𝐺𝑉) ∧ 𝑍 ∈ V) → dom 𝐺 ∈ V)
16 simpr 486 . . . . . 6 (((Fun 𝐺𝐹𝐺𝐺𝑉) ∧ 𝑍 ∈ V) → 𝑍 ∈ V)
1712, 15, 163jca 1129 . . . . 5 (((Fun 𝐺𝐹𝐺𝐺𝑉) ∧ 𝑍 ∈ V) → (dom 𝐹 ⊆ dom 𝐺 ∧ dom 𝐺 ∈ V ∧ 𝑍 ∈ V))
189, 17jca 513 . . . 4 (((Fun 𝐺𝐹𝐺𝐺𝑉) ∧ 𝑍 ∈ V) → ((𝐹 Fn dom 𝐹𝐺 Fn dom 𝐺) ∧ (dom 𝐹 ⊆ dom 𝐺 ∧ dom 𝐺 ∈ V ∧ 𝑍 ∈ V)))
19 funssfv 6909 . . . . . . . . 9 ((Fun 𝐺𝐹𝐺𝑥 ∈ dom 𝐹) → (𝐺𝑥) = (𝐹𝑥))
20193expa 1119 . . . . . . . 8 (((Fun 𝐺𝐹𝐺) ∧ 𝑥 ∈ dom 𝐹) → (𝐺𝑥) = (𝐹𝑥))
21 eqeq1 2737 . . . . . . . . 9 ((𝐺𝑥) = (𝐹𝑥) → ((𝐺𝑥) = 𝑍 ↔ (𝐹𝑥) = 𝑍))
2221biimpd 228 . . . . . . . 8 ((𝐺𝑥) = (𝐹𝑥) → ((𝐺𝑥) = 𝑍 → (𝐹𝑥) = 𝑍))
2320, 22syl 17 . . . . . . 7 (((Fun 𝐺𝐹𝐺) ∧ 𝑥 ∈ dom 𝐹) → ((𝐺𝑥) = 𝑍 → (𝐹𝑥) = 𝑍))
2423ralrimiva 3147 . . . . . 6 ((Fun 𝐺𝐹𝐺) → ∀𝑥 ∈ dom 𝐹((𝐺𝑥) = 𝑍 → (𝐹𝑥) = 𝑍))
25243adant3 1133 . . . . 5 ((Fun 𝐺𝐹𝐺𝐺𝑉) → ∀𝑥 ∈ dom 𝐹((𝐺𝑥) = 𝑍 → (𝐹𝑥) = 𝑍))
2625adantr 482 . . . 4 (((Fun 𝐺𝐹𝐺𝐺𝑉) ∧ 𝑍 ∈ V) → ∀𝑥 ∈ dom 𝐹((𝐺𝑥) = 𝑍 → (𝐹𝑥) = 𝑍))
27 suppfnss 8169 . . . 4 (((𝐹 Fn dom 𝐹𝐺 Fn dom 𝐺) ∧ (dom 𝐹 ⊆ dom 𝐺 ∧ dom 𝐺 ∈ V ∧ 𝑍 ∈ V)) → (∀𝑥 ∈ dom 𝐹((𝐺𝑥) = 𝑍 → (𝐹𝑥) = 𝑍) → (𝐹 supp 𝑍) ⊆ (𝐺 supp 𝑍)))
2818, 26, 27sylc 65 . . 3 (((Fun 𝐺𝐹𝐺𝐺𝑉) ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) ⊆ (𝐺 supp 𝑍))
2928expcom 415 . 2 (𝑍 ∈ V → ((Fun 𝐺𝐹𝐺𝐺𝑉) → (𝐹 supp 𝑍) ⊆ (𝐺 supp 𝑍)))
30 ssid 4003 . . . 4 ∅ ⊆ ∅
31 simpr 486 . . . . . 6 ((𝐹 ∈ V ∧ 𝑍 ∈ V) → 𝑍 ∈ V)
32 supp0prc 8144 . . . . . 6 (¬ (𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) = ∅)
3331, 32nsyl5 159 . . . . 5 𝑍 ∈ V → (𝐹 supp 𝑍) = ∅)
34 simpr 486 . . . . . 6 ((𝐺 ∈ V ∧ 𝑍 ∈ V) → 𝑍 ∈ V)
35 supp0prc 8144 . . . . . 6 (¬ (𝐺 ∈ V ∧ 𝑍 ∈ V) → (𝐺 supp 𝑍) = ∅)
3634, 35nsyl5 159 . . . . 5 𝑍 ∈ V → (𝐺 supp 𝑍) = ∅)
3733, 36sseq12d 4014 . . . 4 𝑍 ∈ V → ((𝐹 supp 𝑍) ⊆ (𝐺 supp 𝑍) ↔ ∅ ⊆ ∅))
3830, 37mpbiri 258 . . 3 𝑍 ∈ V → (𝐹 supp 𝑍) ⊆ (𝐺 supp 𝑍))
3938a1d 25 . 2 𝑍 ∈ V → ((Fun 𝐺𝐹𝐺𝐺𝑉) → (𝐹 supp 𝑍) ⊆ (𝐺 supp 𝑍)))
4029, 39pm2.61i 182 1 ((Fun 𝐺𝐹𝐺𝐺𝑉) → (𝐹 supp 𝑍) ⊆ (𝐺 supp 𝑍))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 397  w3a 1088   = wceq 1542  wcel 2107  wral 3062  Vcvv 3475  wss 3947  c0 4321  dom cdm 5675  Fun wfun 6534   Fn wfn 6535  cfv 6540  (class class class)co 7404   supp csupp 8141
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pr 5426  ax-un 7720
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3777  df-csb 3893  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-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  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-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7407  df-oprab 7408  df-mpo 7409  df-supp 8142
This theorem is referenced by:  tdeglem4  25559  tdeglem4OLD  25560  fsuppss  41014
  Copyright terms: Public domain W3C validator