Theorem fsuppimpd 9381

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 9380	. . 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 2108   class class class wbr 5119  Fun wfun 6525  (class class class)co 7405   supp csupp 8159  Fincfn 8959   finSupp cfsupp 9373

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-iota 6484  df-fun 6533  df-fv 6539  df-ov 7408  df-fsupp 9374

This theorem is referenced by:  fsuppsssupp  9393  fsuppsssuppgd  9394  fsuppxpfi  9397  fsuppun  9399  resfsupp  9408  fsuppmptif  9411  fsuppco  9414  fsuppco2  9415  fsuppcor  9416  cantnfcl  9681  cantnfp1lem1  9692  fsuppmapnn0fiublem  14008  fsuppmapnn0fiub  14009  fsuppmapnn0ub  14013  mndpfsupp  18745  gsumzcl  19892  gsumcl  19896  gsumzadd  19903  gsumzmhm  19918  gsumzoppg  19925  gsum2dlem1  19951  gsum2dlem2  19952  gsum2d  19953  gsumxp2  19961  gsumdixp  20279  lcomfsupp  20859  mptscmfsupp0  20884  regsumsupp  21582  frlmphllem  21740  uvcresum  21753  frlmsslsp  21756  frlmup1  21758  mplcoe1  21995  mplbas2  22000  psrbagev1  22035  evlslem2  22037  evlslem6  22039  psdmplcl  22100  evls1fpws  22307  tsmsgsum  24077  rrxcph  25344  rrxfsupp  25354  mdegldg  26023  mdegcl  26026  plypf1  26169  fsuppinisegfi  32664  fsupprnfi  32669  fsuppcurry1  32702  fsuppcurry2  32703  offinsupp1  32704  gsumfs2d  33049  gsumhashmul  33055  rmfsupp2  33233  elrgspnlem2  33238  elrgspnlem4  33240  elrgspnsubrunlem1  33242  elrgspnsubrunlem2  33243  elrspunidl  33443  elrspunsn  33444  rprmdvdsprod  33549  fedgmullem1  33669  fedgmullem2  33670  evls1fldgencl  33711  fldextrspunlsplem  33714  fldextrspunlsp  33715  zarcmplem  33912  fsuppind  42613  mnringmulrcld  44252  rmfsupp  48348  scmfsupp  48350  lincresunit2  48454