Theorem fsuppimpd 9279

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

Syntax hints:   → wi 4   ∈ wcel 2119   class class class wbr 5079  Fun wfun 6486  (class class class)co 7363   supp csupp 8107  Fincfn 8890   finSupp cfsupp 9271

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-iota 6448  df-fun 6494  df-fv 6500  df-ov 7366  df-fsupp 9272

This theorem is referenced by:  fsuppsssupp  9291  fsuppsssuppgd  9292  fsuppxpfi  9295  fsuppun  9297  resfsupp  9306  fsuppmptif  9309  fsuppco  9312  fsuppco2  9313  fsuppcor  9314  cantnfcl  9586  cantnfp1lem1  9597  fsuppmapnn0fiublem  13950  fsuppmapnn0fiub  13951  fsuppmapnn0ub  13955  mndpfsupp  18733  gsumzcl  19884  gsumcl  19888  gsumzadd  19895  gsumzmhm  19910  gsumzoppg  19917  gsum2dlem1  19943  gsum2dlem2  19944  gsum2d  19945  gsumxp2  19953  gsumdixp  20296  lcomfsupp  20899  mptscmfsupp0  20924  regsumsupp  21604  frlmphllem  21762  uvcresum  21775  frlmsslsp  21778  frlmup1  21780  mplcoe1  22020  mplbas2  22025  psrbagev1  22060  evlslem2  22062  evlslem6  22064  psdmplcl  22157  evls1fpws  22362  tsmsgsum  24129  rrxcph  25384  rrxfsupp  25394  mdegldg  26056  mdegcl  26059  plypf1  26202  fsuppinisegfi  32786  fsupprnfi  32791  fsuppcurry1  32823  fsuppcurry2  32824  offinsupp1  32825  gsumfs2d  33149  gsumhashmul  33155  rmfsupp2  33326  elrgspnlem2  33331  elrgspnlem4  33333  elrgspnsubrunlem1  33335  elrgspnsubrunlem2  33336  elrspunidl  33518  elrspunsn  33519  rprmdvdsprod  33624  extvfvcl  33727  psrmonprod  33743  esplyfval3  33763  esplyind  33766  fedgmullem1  33820  fedgmullem2  33821  evls1fldgencl  33861  fldextrspunlsplem  33864  fldextrspunlsp  33865  zarcmplem  34072  fsuppind  43047  mnringmulrcld  44679  rmfsupp  48871  scmfsupp  48873  lincresunit2  48976