Theorem fsuppimpd 9278

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 9277	. . 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 5095  Fun wfun 6480  (class class class)co 7353   supp csupp 8100  Fincfn 8879   finSupp cfsupp 9270

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 5238  ax-nul 5248  ax-pr 5374

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 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-iota 6442  df-fun 6488  df-fv 6494  df-ov 7356  df-fsupp 9271

This theorem is referenced by:  fsuppsssupp  9290  fsuppsssuppgd  9291  fsuppxpfi  9294  fsuppun  9296  resfsupp  9305  fsuppmptif  9308  fsuppco  9311  fsuppco2  9312  fsuppcor  9313  cantnfcl  9582  cantnfp1lem1  9593  fsuppmapnn0fiublem  13915  fsuppmapnn0fiub  13916  fsuppmapnn0ub  13920  mndpfsupp  18659  gsumzcl  19808  gsumcl  19812  gsumzadd  19819  gsumzmhm  19834  gsumzoppg  19841  gsum2dlem1  19867  gsum2dlem2  19868  gsum2d  19869  gsumxp2  19877  gsumdixp  20222  lcomfsupp  20823  mptscmfsupp0  20848  regsumsupp  21547  frlmphllem  21705  uvcresum  21718  frlmsslsp  21721  frlmup1  21723  mplcoe1  21960  mplbas2  21965  psrbagev1  22000  evlslem2  22002  evlslem6  22004  psdmplcl  22065  evls1fpws  22272  tsmsgsum  24042  rrxcph  25308  rrxfsupp  25318  mdegldg  25987  mdegcl  25990  plypf1  26133  fsuppinisegfi  32643  fsupprnfi  32648  fsuppcurry1  32681  fsuppcurry2  32682  offinsupp1  32683  gsumfs2d  33021  gsumhashmul  33027  rmfsupp2  33188  elrgspnlem2  33193  elrgspnlem4  33195  elrgspnsubrunlem1  33197  elrgspnsubrunlem2  33198  elrspunidl  33375  elrspunsn  33376  rprmdvdsprod  33481  fedgmullem1  33601  fedgmullem2  33602  evls1fldgencl  33641  fldextrspunlsplem  33644  fldextrspunlsp  33645  zarcmplem  33847  fsuppind  42563  mnringmulrcld  44201  rmfsupp  48358  scmfsupp  48360  lincresunit2  48464