Theorem fsuppimpd 9406

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 9405	. . 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 2105   class class class wbr 5147  Fun wfun 6556  (class class class)co 7430   supp csupp 8183  Fincfn 8983   finSupp cfsupp 9398

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-iota 6515  df-fun 6564  df-fv 6570  df-ov 7433  df-fsupp 9399

This theorem is referenced by:  fsuppsssupp  9418  fsuppsssuppgd  9419  fsuppxpfi  9422  fsuppun  9424  resfsupp  9433  fsuppmptif  9436  fsuppco  9439  fsuppco2  9440  fsuppcor  9441  cantnfcl  9704  cantnfp1lem1  9715  fsuppmapnn0fiublem  14027  fsuppmapnn0fiub  14028  fsuppmapnn0ub  14032  mndpfsupp  18792  gsumzcl  19943  gsumcl  19947  gsumzadd  19954  gsumzmhm  19969  gsumzoppg  19976  gsum2dlem1  20002  gsum2dlem2  20003  gsum2d  20004  gsumxp2  20012  gsumdixp  20332  lcomfsupp  20916  mptscmfsupp0  20941  regsumsupp  21657  frlmphllem  21817  uvcresum  21830  frlmsslsp  21833  frlmup1  21835  mplcoe1  22072  mplbas2  22077  psrbagev1  22118  evlslem2  22120  evlslem6  22122  psdmplcl  22183  evls1fpws  22388  tsmsgsum  24162  rrxcph  25439  rrxfsupp  25449  mdegldg  26119  mdegcl  26122  plypf1  26265  fsuppinisegfi  32701  fsupprnfi  32706  fsuppcurry1  32742  fsuppcurry2  32743  offinsupp1  32744  gsumfs2d  33040  gsumhashmul  33046  rmfsupp2  33227  elrgspnlem2  33232  elrgspnlem4  33234  elrspunidl  33435  elrspunsn  33436  rprmdvdsprod  33541  fedgmullem1  33656  fedgmullem2  33657  evls1fldgencl  33694  zarcmplem  33841  fsuppind  42576  mnringmulrcld  44223  rmfsupp  48217  scmfsupp  48219  lincresunit2  48323