Theorem fsuppimpd 9320

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 9319	. . 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 2109   class class class wbr 5107  Fun wfun 6505  (class class class)co 7387   supp csupp 8139  Fincfn 8918   finSupp cfsupp 9312

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-iota 6464  df-fun 6513  df-fv 6519  df-ov 7390  df-fsupp 9313

This theorem is referenced by:  fsuppsssupp  9332  fsuppsssuppgd  9333  fsuppxpfi  9336  fsuppun  9338  resfsupp  9347  fsuppmptif  9350  fsuppco  9353  fsuppco2  9354  fsuppcor  9355  cantnfcl  9620  cantnfp1lem1  9631  fsuppmapnn0fiublem  13955  fsuppmapnn0fiub  13956  fsuppmapnn0ub  13960  mndpfsupp  18694  gsumzcl  19841  gsumcl  19845  gsumzadd  19852  gsumzmhm  19867  gsumzoppg  19874  gsum2dlem1  19900  gsum2dlem2  19901  gsum2d  19902  gsumxp2  19910  gsumdixp  20228  lcomfsupp  20808  mptscmfsupp0  20833  regsumsupp  21531  frlmphllem  21689  uvcresum  21702  frlmsslsp  21705  frlmup1  21707  mplcoe1  21944  mplbas2  21949  psrbagev1  21984  evlslem2  21986  evlslem6  21988  psdmplcl  22049  evls1fpws  22256  tsmsgsum  24026  rrxcph  25292  rrxfsupp  25302  mdegldg  25971  mdegcl  25974  plypf1  26117  fsuppinisegfi  32610  fsupprnfi  32615  fsuppcurry1  32648  fsuppcurry2  32649  offinsupp1  32650  gsumfs2d  32995  gsumhashmul  33001  rmfsupp2  33189  elrgspnlem2  33194  elrgspnlem4  33196  elrgspnsubrunlem1  33198  elrgspnsubrunlem2  33199  elrspunidl  33399  elrspunsn  33400  rprmdvdsprod  33505  fedgmullem1  33625  fedgmullem2  33626  evls1fldgencl  33665  fldextrspunlsplem  33668  fldextrspunlsp  33669  zarcmplem  33871  fsuppind  42578  mnringmulrcld  44217  rmfsupp  48361  scmfsupp  48363  lincresunit2  48467