Theorem fsuppimpd 9400

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 9399	. . 3 ⊢ (𝐹 finSupp 𝑍 → (Fun 𝐹 ∧ (𝐹 supp 𝑍) ∈ Fin))
3	2	simprd 494	. 2 ⊢ (𝐹 finSupp 𝑍 → (𝐹 supp 𝑍) ∈ Fin)
4	1, 3	syl 17	1 ⊢ (𝜑 → (𝐹 supp 𝑍) ∈ Fin)

Syntax hints:   → wi 4   ∈ wcel 2098   class class class wbr 5149  Fun wfun 6543  (class class class)co 7419   supp csupp 8165  Fincfn 8964   finSupp cfsupp 9392

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pr 5429

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-br 5150  df-opab 5212  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-iota 6501  df-fun 6551  df-fv 6557  df-ov 7422  df-fsupp 9393

This theorem is referenced by:  fsuppsssupp  9411  fsuppsssuppgd  9412  fsuppxpfi  9415  fsuppun  9417  resfsupp  9426  fsuppmptif  9429  fsuppco  9432  fsuppco2  9433  fsuppcor  9434  cantnfcl  9697  cantnfp1lem1  9708  fsuppmapnn0fiublem  13996  fsuppmapnn0fiub  13997  fsuppmapnn0ub  14001  gsumzcl  19883  gsumcl  19887  gsumzadd  19894  gsumzmhm  19909  gsumzoppg  19916  gsum2dlem1  19942  gsum2dlem2  19943  gsum2d  19944  gsumxp2  19952  gsumdixp  20272  lcomfsupp  20802  mptscmfsupp0  20827  regsumsupp  21576  frlmphllem  21736  uvcresum  21749  frlmsslsp  21752  frlmup1  21754  mplcoe1  22002  mplbas2  22007  psrbagev1  22048  psrbagev1OLD  22049  evlslem2  22052  evlslem6  22054  psdmplcl  22114  evls1fpws  22318  tsmsgsum  24092  rrxcph  25369  rrxfsupp  25379  mdegldg  26051  mdegcl  26054  plypf1  26196  fsuppinisegfi  32554  fsupprnfi  32559  fsuppcurry1  32594  fsuppcurry2  32595  offinsupp1  32596  gsumhashmul  32865  rmfsupp2  33043  elrspunidl  33245  elrspunsn  33246  rprmdvdsprod  33351  fedgmullem1  33460  fedgmullem2  33461  evls1fldgencl  33491  zarcmplem  33615  fsuppind  41960  mnringmulrcld  43809  rmfsupp  47626  mndpfsupp  47628  scmfsupp  47630  lincresunit2  47734