Theorem fsuppimpd 9284

Description: A finitely supported function is a function with a finite support. (Contributed by AV, 6-Jun-2019.)

Hypothesis

Ref	Expression
fsuppimpd.f	⊢ (𝜑 → 𝐹 finSupp 𝑍)

Assertion

Ref	Expression
fsuppimpd	⊢ (𝜑 → (𝐹 supp 𝑍) ∈ Fin)

Proof of Theorem fsuppimpd

Step	Hyp	Ref	Expression
1		fsuppimpd.f	. 2 ⊢ (𝜑 → 𝐹 finSupp 𝑍)
2		fsuppimp 9283	. . 3 ⊢ (𝐹 finSupp 𝑍 → (Fun 𝐹 ∧ (𝐹 supp 𝑍) ∈ Fin))
3	2	simprd 495	. 2 ⊢ (𝐹 finSupp 𝑍 → (𝐹 supp 𝑍) ∈ Fin)
4	1, 3	syl 17	1 ⊢ (𝜑 → (𝐹 supp 𝑍) ∈ Fin)

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5100  Fun wfun 6494  (class class class)co 7368   supp csupp 8112  Fincfn 8895   finSupp cfsupp 9276

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-iota 6456  df-fun 6502  df-fv 6508  df-ov 7371  df-fsupp 9277

This theorem is referenced by:  fsuppsssupp  9296  fsuppsssuppgd  9297  fsuppxpfi  9300  fsuppun  9302  resfsupp  9311  fsuppmptif  9314  fsuppco  9317  fsuppco2  9318  fsuppcor  9319  cantnfcl  9588  cantnfp1lem1  9599  fsuppmapnn0fiublem  13925  fsuppmapnn0fiub  13926  fsuppmapnn0ub  13930  mndpfsupp  18704  gsumzcl  19852  gsumcl  19856  gsumzadd  19863  gsumzmhm  19878  gsumzoppg  19885  gsum2dlem1  19911  gsum2dlem2  19912  gsum2d  19913  gsumxp2  19921  gsumdixp  20266  lcomfsupp  20865  mptscmfsupp0  20890  regsumsupp  21589  frlmphllem  21747  uvcresum  21760  frlmsslsp  21763  frlmup1  21765  mplcoe1  22004  mplbas2  22009  psrbagev1  22044  evlslem2  22046  evlslem6  22048  psdmplcl  22117  evls1fpws  22325  tsmsgsum  24095  rrxcph  25360  rrxfsupp  25370  mdegldg  26039  mdegcl  26042  plypf1  26185  fsuppinisegfi  32776  fsupprnfi  32781  fsuppcurry1  32813  fsuppcurry2  32814  offinsupp1  32815  gsumfs2d  33154  gsumhashmul  33160  rmfsupp2  33331  elrgspnlem2  33336  elrgspnlem4  33338  elrgspnsubrunlem1  33340  elrgspnsubrunlem2  33341  elrspunidl  33520  elrspunsn  33521  rprmdvdsprod  33626  extvfvcl  33712  psrmonprod  33728  esplyfval3  33748  esplyind  33751  fedgmullem1  33806  fedgmullem2  33807  evls1fldgencl  33847  fldextrspunlsplem  33850  fldextrspunlsp  33851  zarcmplem  34058  fsuppind  42942  mnringmulrcld  44578  rmfsupp  48727  scmfsupp  48729  lincresunit2  48832