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

Theorem suppssdm 7173
Description: The support of a function is a subset of the function's domain. (Contributed by AV, 30-May-2019.)
Assertion
Ref Expression
suppssdm (𝐹 supp 𝑍) ⊆ dom 𝐹

Proof of Theorem suppssdm
Dummy variable 𝑖 is distinct from all other variables.
StepHypRef Expression
1 suppval 7162 . . 3 ((𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) = {𝑖 ∈ dom 𝐹 ∣ (𝐹 “ {𝑖}) ≠ {𝑍}})
2 ssrab2 3650 . . 3 {𝑖 ∈ dom 𝐹 ∣ (𝐹 “ {𝑖}) ≠ {𝑍}} ⊆ dom 𝐹
31, 2syl6eqss 3618 . 2 ((𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) ⊆ dom 𝐹)
4 supp0prc 7163 . . 3 (¬ (𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) = ∅)
5 0ss 3924 . . 3 ∅ ⊆ dom 𝐹
64, 5syl6eqss 3618 . 2 (¬ (𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) ⊆ dom 𝐹)
73, 6pm2.61i 175 1 (𝐹 supp 𝑍) ⊆ dom 𝐹
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 383  wcel 1977  wne 2780  {crab 2900  Vcvv 3173  wss 3540  c0 3874  {csn 4125  dom cdm 5028  cima 5031  (class class class)co 6527   supp csupp 7160
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4704  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6825
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4368  df-br 4579  df-opab 4639  df-id 4943  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-iota 5754  df-fun 5792  df-fv 5798  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-supp 7161
This theorem is referenced by:  snopsuppss  7175  wemapso2lem  8318  cantnfcl  8425  cantnfle  8429  cantnflt  8430  cantnff  8432  cantnfres  8435  cantnfp1lem2  8437  cantnfp1lem3  8438  cantnflem1b  8444  cantnflem1d  8446  cantnflem1  8447  cantnflem3  8449  cnfcomlem  8457  cnfcom  8458  cnfcom2lem  8459  cnfcom3lem  8461  cnfcom3  8462  fsuppmapnn0fiublem  12609  fsuppmapnn0fiub  12610  fsuppmapnn0fiubOLD  12611  gsumval3lem1  18078  gsumval3lem2  18079  gsumval3  18080  gsumzres  18082  gsumzcl2  18083  gsumzf1o  18085  gsumzaddlem  18093  gsumconst  18106  gsumzoppg  18116  gsum2d  18143  dpjidcl  18229  psrass1lem  19147  psrass1  19175  psrass23l  19178  psrcom  19179  psrass23  19180  mplcoe1  19235  psropprmul  19378  coe1mul2  19409  gsumfsum  19581  regsumsupp  19735  frlmlbs  19903  tsmsgsum  21700  rrxcph  22933  rrxsuppss  22939  rrxmval  22941  mdegfval  23571  mdegleb  23573  mdegldg  23575  deg1mul3le  23625  wilthlem3  24541  fdivmpt  42124  fdivmptf  42125  refdivmptf  42126  fdivpm  42127  refdivpm  42128
  Copyright terms: Public domain W3C validator