Theorem fsuppimpd 9312

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 9311	. . 3 ⊢ (𝐹 finSupp 𝑍 → (Fun 𝐹 ∧ (𝐹 supp 𝑍) ∈ Fin))
3	2	simprd 499	. 2 ⊢ (𝐹 finSupp 𝑍 → (𝐹 supp 𝑍) ∈ Fin)
4	1, 3	syl 17	1 ⊢ (𝜑 → (𝐹 supp 𝑍) ∈ Fin)

Syntax hints:   → wi 4   ∈ wcel 2141   class class class wbr 5099  Fun wfun 6511  (class class class)co 7392   supp csupp 8135  Fincfn 8923   finSupp cfsupp 9304

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5245  ax-pr 5389

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-iota 6473  df-fun 6519  df-fv 6525  df-ov 7395  df-fsupp 9305

This theorem is referenced by:  fsuppsssupp  9324  fsuppsssuppgd  9325  fsuppxpfi  9328  fsuppun  9330  resfsupp  9339  fsuppmptif  9342  fsuppco  9345  fsuppco2  9346  fsuppcor  9347  cantnfcl  9619  cantnfp1lem1  9630  fsuppmapnn0fiublem  14000  fsuppmapnn0fiub  14001  fsuppmapnn0ub  14005  mndpfsupp  18784  gsumzcl  19934  gsumcl  19938  gsumzadd  19945  gsumzmhm  19960  gsumzoppg  19967  gsum2dlem1  19993  gsum2dlem2  19994  gsum2d  19995  gsumxp2  20003  gsumdixp  20346  lcomfsupp  20949  mptscmfsupp0  20974  regsumsupp  21654  frlmphllem  21812  uvcresum  21825  frlmsslsp  21828  frlmup1  21830  mplcoe1  22070  mplbas2  22075  psrbagev1  22110  evlslem2  22112  evlslem6  22114  psdmplcl  22207  evls1fpws  22412  tsmsgsum  24179  rrxcph  25434  rrxfsupp  25444  mdegldg  26106  mdegcl  26109  plypf1  26252  fsuppinisegfi  32839  fsupprnfi  32844  fsuppcurry1  32876  fsuppcurry2  32877  offinsupp1  32878  gsumfs2d  33202  gsumhashmul  33208  rmfsupp2  33379  elrgspnlem2  33385  elrgspnlem4  33387  elrgspnsubrunlem1  33389  elrgspnsubrunlem2  33390  elrspunidl  33575  elrspunsn  33576  rprmdvdsprod  33691  extvfvcl  33794  psrmonprod  33810  esplyfval3  33830  esplyind  33833  fedgmullem1  33887  fedgmullem2  33888  evls1fldgencl  33928  fldextrspunlsplem  33931  fldextrspunlsp  33932  zarcmplem  34139  fsuppind  43136  mnringmulrcld  44768  rmfsupp  48959  scmfsupp  48961  lincresunit2  49064