Theorem fsuppimpd 9389

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 9388	. . 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 2147   class class class wbr 5106  Fun wfun 6552  (class class class)co 7443   supp csupp 8204  Fincfn 9001   finSupp cfsupp 9381

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252  ax-pr 5395

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-iota 6512  df-fun 6560  df-fv 6566  df-ov 7446  df-fsupp 9382

This theorem is used by:  fsuppsssupp  9400  fsuppsssuppgd  9401  fsuppxpfi  9404  fsuppun  9406  resfsupp  9415  fsuppmptif  9418  fsuppco  9421  fsuppco2  9422  fsuppcor  9423  cantnfcl  9695  cantnfp1lem1  9706  fsuppmapnn0fiublem  14160  fsuppmapnn0fiub  14161  fsuppmapnn0ub  14165  mndpfsupp  18990  gsumzcl  20155  gsumcl  20159  gsumzadd  20166  gsumzmhm  20181  gsumzoppg  20188  gsum2dlem1  20214  gsum2dlem2  20215  gsum2d  20216  gsumxp2  20224  gsumdixp  20578  lcomfsupp  21207  mptscmfsupp0  21232  regsumsupp  21958  frlmphllem  22116  uvcresum  22129  frlmsslsp  22132  frlmup1  22134  mplcoe1  22376  mplbas2  22381  psrbagev1  22416  evlslem2  22418  evlslem6  22420  psdmplcl  22513  evls1fpws  22717  tsmsgsum  24488  rrxcph  25743  rrxfsupp  25753  mdegldg  26414  mdegcl  26417  plypf1  26561  fsuppinisegfi  33351  fsupprnfi  33356  fsuppcurry1  33386  fsuppcurry2  33387  offinsupp1  33388  gsumfs2d  33692  gsumhashmul  33698  rmfsupp2  33868  elrgspnlem2  33874  elrgspnlem4  33876  elrgspnsubrunlem1  33878  elrgspnsubrunlem2  33879  elrspunidl  34048  elrspunsn  34049  rprmdvdsprod  34136  extvfvcl  34238  psrmonprod  34254  esplyfval3  34274  esplyind  34277  fedgmullem1  34331  fedgmullem2  34332  evls1fldgencl  34372  fldextrspunlsplem  34375  fldextrspunlsp  34376  zarcmplem  34583  fsuppind  43811  mnringmulrcld  45418  rmfsupp  49690  scmfsupp  49692  lincresunit2  49795