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

Theorem fsuppimpd 7846
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 7845 . . 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 1767   class class class wbr 4452   Fun wfun 5587  (class class class)co 6294   supp csupp 6911   Fincfn 7526   finSupp cfsupp 7839
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  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 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2822  df-rex 2823  df-rab 2826  df-v 3120  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-nul 3791  df-if 3945  df-sn 4033  df-pr 4035  df-op 4039  df-uni 4251  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 6297  df-fsupp 7840
This theorem is referenced by:  fsuppsssupp  7855  fsuppxpfi  7856  fsuppun  7858  fsuppmptif  7869  fsuppco2  7872  fsuppcor  7873  cantnfcl  8096  cantnfp1lem1  8107  fsuppmapnn0fiublem  12074  fsuppmapnn0fiub  12075  fsuppmapnn0ub  12079  gsumzcl  16766  gsumcl  16773  gsumzmhm  16807  gsumzoppg  16817  gsum2dlem1  16847  gsum2dlem2  16848  gsum2d  16849  gsumdixp  17107  lcomfsupp  17398  mptscmfsupp0  17424  mplcoe1  17974  mplbas2  17981  psrbagev1  18024  evlslem2  18027  evlslem6  18028  ply1coeOLD  18185  regsumsupp  18504  frlmphllem  18657  uvcresum  18670  frlmsslsp  18675  frlmup1  18678  tsmsgsum  20482  rrxcph  21669  mdegcl  22314  plypf1  22454  rmfsupp  32341  mndpfsupp  32343  scmfsupp  32345  lincresunit2  32453
  Copyright terms: Public domain W3C validator