Theorem fsuppimpd 9275

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 9274	. . 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 5086  Fun wfun 6486  (class class class)co 7360   supp csupp 8103  Fincfn 8886   finSupp cfsupp 9267

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 5231  ax-pr 5370

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-iota 6448  df-fun 6494  df-fv 6500  df-ov 7363  df-fsupp 9268

This theorem is referenced by:  fsuppsssupp  9287  fsuppsssuppgd  9288  fsuppxpfi  9291  fsuppun  9293  resfsupp  9302  fsuppmptif  9305  fsuppco  9308  fsuppco2  9309  fsuppcor  9310  cantnfcl  9579  cantnfp1lem1  9590  fsuppmapnn0fiublem  13943  fsuppmapnn0fiub  13944  fsuppmapnn0ub  13948  mndpfsupp  18726  gsumzcl  19877  gsumcl  19881  gsumzadd  19888  gsumzmhm  19903  gsumzoppg  19910  gsum2dlem1  19936  gsum2dlem2  19937  gsum2d  19938  gsumxp2  19946  gsumdixp  20289  lcomfsupp  20888  mptscmfsupp0  20913  regsumsupp  21612  frlmphllem  21770  uvcresum  21783  frlmsslsp  21786  frlmup1  21788  mplcoe1  22025  mplbas2  22030  psrbagev1  22065  evlslem2  22067  evlslem6  22069  psdmplcl  22138  evls1fpws  22344  tsmsgsum  24114  rrxcph  25369  rrxfsupp  25379  mdegldg  26041  mdegcl  26044  plypf1  26187  fsuppinisegfi  32775  fsupprnfi  32780  fsuppcurry1  32812  fsuppcurry2  32813  offinsupp1  32814  gsumfs2d  33137  gsumhashmul  33143  rmfsupp2  33314  elrgspnlem2  33319  elrgspnlem4  33321  elrgspnsubrunlem1  33323  elrgspnsubrunlem2  33324  elrspunidl  33503  elrspunsn  33504  rprmdvdsprod  33609  extvfvcl  33695  psrmonprod  33711  esplyfval3  33731  esplyind  33734  fedgmullem1  33789  fedgmullem2  33790  evls1fldgencl  33830  fldextrspunlsplem  33833  fldextrspunlsp  33834  zarcmplem  34041  fsuppind  43037  mnringmulrcld  44673  rmfsupp  48861  scmfsupp  48863  lincresunit2  48966