Theorem fsuppimpd 9272

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 9271	. . 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 2113   class class class wbr 5098  Fun wfun 6486  (class class class)co 7358   supp csupp 8102  Fincfn 8883   finSupp cfsupp 9264

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-iota 6448  df-fun 6494  df-fv 6500  df-ov 7361  df-fsupp 9265

This theorem is referenced by:  fsuppsssupp  9284  fsuppsssuppgd  9285  fsuppxpfi  9288  fsuppun  9290  resfsupp  9299  fsuppmptif  9302  fsuppco  9305  fsuppco2  9306  fsuppcor  9307  cantnfcl  9576  cantnfp1lem1  9587  fsuppmapnn0fiublem  13913  fsuppmapnn0fiub  13914  fsuppmapnn0ub  13918  mndpfsupp  18692  gsumzcl  19840  gsumcl  19844  gsumzadd  19851  gsumzmhm  19866  gsumzoppg  19873  gsum2dlem1  19899  gsum2dlem2  19900  gsum2d  19901  gsumxp2  19909  gsumdixp  20254  lcomfsupp  20853  mptscmfsupp0  20878  regsumsupp  21577  frlmphllem  21735  uvcresum  21748  frlmsslsp  21751  frlmup1  21753  mplcoe1  21992  mplbas2  21997  psrbagev1  22032  evlslem2  22034  evlslem6  22036  psdmplcl  22105  evls1fpws  22313  tsmsgsum  24083  rrxcph  25348  rrxfsupp  25358  mdegldg  26027  mdegcl  26030  plypf1  26173  fsuppinisegfi  32766  fsupprnfi  32771  fsuppcurry1  32803  fsuppcurry2  32804  offinsupp1  32805  gsumfs2d  33144  gsumhashmul  33150  rmfsupp2  33320  elrgspnlem2  33325  elrgspnlem4  33327  elrgspnsubrunlem1  33329  elrgspnsubrunlem2  33330  elrspunidl  33509  elrspunsn  33510  rprmdvdsprod  33615  extvfvcl  33701  esplyfval3  33730  esplyind  33731  fedgmullem1  33786  fedgmullem2  33787  evls1fldgencl  33827  fldextrspunlsplem  33830  fldextrspunlsp  33831  zarcmplem  34038  fsuppind  42829  mnringmulrcld  44465  rmfsupp  48615  scmfsupp  48617  lincresunit2  48720