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

Theorem fsuppimpd 7856
Description: A finitely supported function is a function with a finite support. (Contributed by AV, 6-Jun-2019.)
Hypothesis
Ref Expression
fsuppimpd.f
Assertion
Ref Expression
fsuppimpd

Proof of Theorem fsuppimpd
StepHypRef Expression
1 fsuppimpd.f . 2
2 fsuppimp 7855 . . 3
32simprd 463 . 2
41, 3syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1818   class class class wbr 4452  Funwfun 5587  (class class class)co 6296   csupp 6918   cfn 7536   cfsupp 7849
This theorem is referenced by:  fsuppsssupp  7865  fsuppxpfi  7866  fsuppun  7868  resfsupp  7876  fsuppmptif  7879  fsuppco  7881  fsuppco2  7882  fsuppcor  7883  cantnfcl  8107  cantnfp1lem1  8118  fsuppmapnn0fiublem  12096  fsuppmapnn0fiub  12097  fsuppmapnn0ub  12101  gsumzcl  16916  gsumcl  16923  gsumzadd  16935  gsumzmhm  16957  gsumzoppg  16967  gsum2dlem1  16997  gsum2dlem2  16998  gsum2d  16999  gsumdixp  17258  lcomfsupp  17550  mptscmfsupp0  17576  mplcoe1  18127  mplbas2  18134  psrbagev1  18177  evlslem2  18180  evlslem6  18181  ply1coeOLD  18338  regsumsupp  18658  frlmphllem  18811  uvcresum  18824  frlmsslsp  18829  frlmup1  18832  tsmsgsum  20637  rrxcph  21824  rrxfsupp  21829  mdegldg  22466  mdegcl  22469  plypf1  22609  rmfsupp  32967  mndpfsupp  32969  scmfsupp  32971  lincresunit2  33079
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-iota 5556  df-fun 5595  df-fv 5601  df-ov 6299  df-fsupp 7850
  Copyright terms: Public domain W3C validator