Theorem fsuppimpd 9345

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 9344	. . 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 2145   class class class wbr 5103  Fun wfun 6525  (class class class)co 7412   supp csupp 8161  Fincfn 8957   finSupp cfsupp 9337

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-iota 6487  df-fun 6533  df-fv 6539  df-ov 7415  df-fsupp 9338

This theorem is used by:  fsuppsssupp  9357  fsuppsssuppgd  9358  fsuppxpfi  9361  fsuppun  9363  resfsupp  9372  fsuppmptif  9375  fsuppco  9378  fsuppco2  9379  fsuppcor  9380  cantnfcl  9652  cantnfp1lem1  9663  fsuppmapnn0fiublem  14113  fsuppmapnn0fiub  14114  fsuppmapnn0ub  14118  mndpfsupp  18941  gsumzcl  20105  gsumcl  20109  gsumzadd  20116  gsumzmhm  20131  gsumzoppg  20138  gsum2dlem1  20164  gsum2dlem2  20165  gsum2d  20166  gsumxp2  20174  gsumdixp  20528  lcomfsupp  21157  mptscmfsupp0  21182  regsumsupp  21908  frlmphllem  22066  uvcresum  22079  frlmsslsp  22082  frlmup1  22084  mplcoe1  22326  mplbas2  22331  psrbagev1  22366  evlslem2  22368  evlslem6  22370  psdmplcl  22463  evls1fpws  22667  tsmsgsum  24438  rrxcph  25693  rrxfsupp  25703  mdegldg  26364  mdegcl  26367  plypf1  26511  fsuppinisegfi  33262  fsupprnfi  33267  fsuppcurry1  33298  fsuppcurry2  33299  offinsupp1  33300  gsumfs2d  33604  gsumhashmul  33610  rmfsupp2  33780  elrgspnlem2  33786  elrgspnlem4  33788  elrgspnsubrunlem1  33790  elrgspnsubrunlem2  33791  elrspunidl  33960  elrspunsn  33961  rprmdvdsprod  34048  extvfvcl  34150  psrmonprod  34166  esplyfval3  34186  esplyind  34189  fedgmullem1  34243  fedgmullem2  34244  evls1fldgencl  34284  fldextrspunlsplem  34287  fldextrspunlsp  34288  zarcmplem  34495  fsuppind  43580  mnringmulrcld  45185  rmfsupp  49429  scmfsupp  49431  lincresunit2  49534