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

Theorem fsuppimpd 7834
Description: A finitely supported function is a function with a finite support. (Contributed by AV, 6-Jun-2019.)
Hypothesis
Ref Expression
fsuppimpd.f  |-  ( ph  ->  F finSupp  Z )
Assertion
Ref Expression
fsuppimpd  |-  ( ph  ->  ( F supp  Z )  e.  Fin )

Proof of Theorem fsuppimpd
StepHypRef Expression
1 fsuppimpd.f . 2  |-  ( ph  ->  F finSupp  Z )
2 fsuppimp 7833 . . 3  |-  ( F finSupp  Z  ->  ( Fun  F  /\  ( F supp  Z )  e.  Fin ) )
32simprd 463 . 2  |-  ( F finSupp  Z  ->  ( F supp  Z
)  e.  Fin )
41, 3syl 16 1  |-  ( ph  ->  ( F supp  Z )  e.  Fin )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1802   class class class wbr 4433   Fun wfun 5568  (class class class)co 6277   supp csupp 6899   Fincfn 7514   finSupp cfsupp 7827
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4554  ax-nul 4562  ax-pr 4672
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3095  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768  df-if 3923  df-sn 4011  df-pr 4013  df-op 4017  df-uni 4231  df-br 4434  df-opab 4492  df-xp 4991  df-rel 4992  df-cnv 4993  df-co 4994  df-iota 5537  df-fun 5576  df-fv 5582  df-ov 6280  df-fsupp 7828
This theorem is referenced by:  fsuppsssupp  7843  fsuppxpfi  7844  fsuppun  7846  resfsupp  7854  fsuppmptif  7857  fsuppco  7859  fsuppco2  7860  fsuppcor  7861  cantnfcl  8084  cantnfp1lem1  8095  fsuppmapnn0fiublem  12070  fsuppmapnn0fiub  12071  fsuppmapnn0ub  12075  gsumzcl  16785  gsumcl  16792  gsumzadd  16804  gsumzmhm  16826  gsumzoppg  16836  gsum2dlem1  16866  gsum2dlem2  16867  gsum2d  16868  gsumdixp  17126  lcomfsupp  17418  mptscmfsupp0  17444  mplcoe1  17995  mplbas2  18002  psrbagev1  18045  evlslem2  18048  evlslem6  18049  ply1coeOLD  18206  regsumsupp  18525  frlmphllem  18678  uvcresum  18691  frlmsslsp  18696  frlmup1  18699  tsmsgsum  20503  rrxcph  21690  rrxfsupp  21695  mdegldg  22332  mdegcl  22335  plypf1  22475  rmfsupp  32677  mndpfsupp  32679  scmfsupp  32681  lincresunit2  32789
  Copyright terms: Public domain W3C validator