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

Theorem suppssdm 6830
Description: The support of a function is a subset of the function's domain. (Contributed by AV, 30-May-2019.)
Assertion
Ref Expression
suppssdm  |-  ( F supp 
Z )  C_  dom  F

Proof of Theorem suppssdm
Dummy variable  i is distinct from all other variables.
StepHypRef Expression
1 suppval 6819 . . 3  |-  ( ( F  e.  _V  /\  Z  e.  _V )  ->  ( F supp  Z )  =  { i  e. 
dom  F  |  ( F " { i } )  =/=  { Z } } )
2 ssrab2 3499 . . 3  |-  { i  e.  dom  F  | 
( F " {
i } )  =/= 
{ Z } }  C_ 
dom  F
31, 2syl6eqss 3467 . 2  |-  ( ( F  e.  _V  /\  Z  e.  _V )  ->  ( F supp  Z ) 
C_  dom  F )
4 supp0prc 6820 . . 3  |-  ( -.  ( F  e.  _V  /\  Z  e.  _V )  ->  ( F supp  Z )  =  (/) )
5 0ss 3741 . . 3  |-  (/)  C_  dom  F
64, 5syl6eqss 3467 . 2  |-  ( -.  ( F  e.  _V  /\  Z  e.  _V )  ->  ( F supp  Z ) 
C_  dom  F )
73, 6pm2.61i 164 1  |-  ( F supp 
Z )  C_  dom  F
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    /\ wa 367    e. wcel 1826    =/= wne 2577   {crab 2736   _Vcvv 3034    C_ wss 3389   (/)c0 3711   {csn 3944   dom cdm 4913   "cima 4916  (class class class)co 6196   supp csupp 6817
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-8 1828  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pow 4543  ax-pr 4601  ax-un 6491
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-ral 2737  df-rex 2738  df-rab 2741  df-v 3036  df-sbc 3253  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-sn 3945  df-pr 3947  df-op 3951  df-uni 4164  df-br 4368  df-opab 4426  df-id 4709  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926  df-iota 5460  df-fun 5498  df-fv 5504  df-ov 6199  df-oprab 6200  df-mpt2 6201  df-supp 6818
This theorem is referenced by:  snopsuppss  6832  wemapso2lem  7893  cantnfcl  7999  cantnfle  8003  cantnflt  8004  cantnff  8006  cantnfres  8009  cantnfp1lem2  8011  cantnfp1lem3  8012  cantnflem1b  8018  cantnflem1d  8020  cantnflem1  8021  cantnflem3  8023  cnfcomlem  8056  cnfcom  8057  cnfcom2lem  8058  cnfcom3lem  8060  cnfcom3  8061  fsuppmapnn0fiublem  11999  fsuppmapnn0fiub  12000  gsumval3lem1  17026  gsumval3lem2  17027  gsumval3  17028  gsumzres  17031  gsumzcl2  17032  gsumzf1o  17034  gsumzaddlem  17051  gsumconst  17070  gsumzoppg  17083  gsum2d  17113  dpjidcl  17220  psrass1lem  18142  psrass1  18173  psrass23l  18176  psrcom  18177  psrass23  18178  mplcoe1  18240  psropprmul  18392  coe1mul2  18423  gsumfsum  18597  regsumsupp  18749  frlmlbs  18917  tsmsgsum  20722  rrxcph  21909  rrxsuppss  21915  rrxmval  21917  mdegfval  22545  mdegleb  22549  mdegldg  22551  deg1mul3le  22602  wilthlem3  23461  fdivmpt  33361  fdivmptf  33362  refdivmptf  33363  fdivpm  33364  refdivpm  33365
  Copyright terms: Public domain W3C validator