Theorem fsuppimpd 9260

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 9259	. . 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 2113   class class class wbr 5093  Fun wfun 6480  (class class class)co 7352   supp csupp 8096  Fincfn 8875   finSupp cfsupp 9252

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pr 5372

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-iota 6442  df-fun 6488  df-fv 6494  df-ov 7355  df-fsupp 9253

This theorem is referenced by:  fsuppsssupp  9272  fsuppsssuppgd  9273  fsuppxpfi  9276  fsuppun  9278  resfsupp  9287  fsuppmptif  9290  fsuppco  9293  fsuppco2  9294  fsuppcor  9295  cantnfcl  9564  cantnfp1lem1  9575  fsuppmapnn0fiublem  13899  fsuppmapnn0fiub  13900  fsuppmapnn0ub  13904  mndpfsupp  18677  gsumzcl  19825  gsumcl  19829  gsumzadd  19836  gsumzmhm  19851  gsumzoppg  19858  gsum2dlem1  19884  gsum2dlem2  19885  gsum2d  19886  gsumxp2  19894  gsumdixp  20239  lcomfsupp  20837  mptscmfsupp0  20862  regsumsupp  21561  frlmphllem  21719  uvcresum  21732  frlmsslsp  21735  frlmup1  21737  mplcoe1  21973  mplbas2  21978  psrbagev1  22013  evlslem2  22015  evlslem6  22017  psdmplcl  22078  evls1fpws  22285  tsmsgsum  24055  rrxcph  25320  rrxfsupp  25330  mdegldg  25999  mdegcl  26002  plypf1  26145  fsuppinisegfi  32672  fsupprnfi  32677  fsuppcurry1  32711  fsuppcurry2  32712  offinsupp1  32713  gsumfs2d  33042  gsumhashmul  33048  rmfsupp2  33212  elrgspnlem2  33217  elrgspnlem4  33219  elrgspnsubrunlem1  33221  elrgspnsubrunlem2  33222  elrspunidl  33400  elrspunsn  33401  rprmdvdsprod  33506  extvfvcl  33587  esplyfval3  33612  esplyind  33613  fedgmullem1  33663  fedgmullem2  33664  evls1fldgencl  33704  fldextrspunlsplem  33707  fldextrspunlsp  33708  zarcmplem  33915  fsuppind  42708  mnringmulrcld  44345  rmfsupp  48497  scmfsupp  48499  lincresunit2  48603