Theorem fsuppimpd 9364

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144   class class class wbr 5102  Fun wfun 6532  (class class class)co 7420   supp csupp 8179  Fincfn 8976   finSupp cfsupp 9356

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-iota 6494  df-fun 6540  df-fv 6546  df-ov 7423  df-fsupp 9357

This theorem is used by:  fsuppsssupp  9376  fsuppsssuppgd  9377  fsuppxpfi  9380  fsuppun  9382  resfsupp  9391  fsuppmptif  9394  fsuppco  9397  fsuppco2  9398  fsuppcor  9399  cantnfcl  9671  cantnfp1lem1  9682  fsuppmapnn0fiublem  14136  fsuppmapnn0fiub  14137  fsuppmapnn0ub  14141  mndpfsupp  18966  gsumzcl  20130  gsumcl  20134  gsumzadd  20141  gsumzmhm  20156  gsumzoppg  20163  gsum2dlem1  20189  gsum2dlem2  20190  gsum2d  20191  gsumxp2  20199  gsumdixp  20553  lcomfsupp  21182  mptscmfsupp0  21207  regsumsupp  21933  frlmphllem  22091  uvcresum  22104  frlmsslsp  22107  frlmup1  22109  mplcoe1  22351  mplbas2  22356  psrbagev1  22391  evlslem2  22393  evlslem6  22395  psdmplcl  22488  evls1fpws  22692  tsmsgsum  24463  rrxcph  25718  rrxfsupp  25728  mdegldg  26389  mdegcl  26392  plypf1  26536  fsuppinisegfi  33327  fsupprnfi  33332  fsuppcurry1  33362  fsuppcurry2  33363  offinsupp1  33364  gsumfs2d  33668  gsumhashmul  33674  rmfsupp2  33844  elrgspnlem2  33850  elrgspnlem4  33852  elrgspnsubrunlem1  33854  elrgspnsubrunlem2  33855  elrspunidl  34024  elrspunsn  34025  rprmdvdsprod  34112  extvfvcl  34214  psrmonprod  34230  esplyfval3  34250  esplyind  34253  fedgmullem1  34307  fedgmullem2  34308  evls1fldgencl  34348  fldextrspunlsplem  34351  fldextrspunlsp  34352  zarcmplem  34559  fsuppind  43711  mnringmulrcld  45319  rmfsupp  49578  scmfsupp  49580  lincresunit2  49683