Theorem fsuppimpd 9439

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 9438	. . 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 5166  Fun wfun 6567  (class class class)co 7448   supp csupp 8201  Fincfn 9003   finSupp cfsupp 9431

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-iota 6525  df-fun 6575  df-fv 6581  df-ov 7451  df-fsupp 9432

This theorem is referenced by:  fsuppsssupp  9450  fsuppsssuppgd  9451  fsuppxpfi  9454  fsuppun  9456  resfsupp  9465  fsuppmptif  9468  fsuppco  9471  fsuppco2  9472  fsuppcor  9473  cantnfcl  9736  cantnfp1lem1  9747  fsuppmapnn0fiublem  14041  fsuppmapnn0fiub  14042  fsuppmapnn0ub  14046  gsumzcl  19953  gsumcl  19957  gsumzadd  19964  gsumzmhm  19979  gsumzoppg  19986  gsum2dlem1  20012  gsum2dlem2  20013  gsum2d  20014  gsumxp2  20022  gsumdixp  20342  lcomfsupp  20922  mptscmfsupp0  20947  regsumsupp  21663  frlmphllem  21823  uvcresum  21836  frlmsslsp  21839  frlmup1  21841  mplcoe1  22078  mplbas2  22083  psrbagev1  22124  evlslem2  22126  evlslem6  22128  psdmplcl  22189  evls1fpws  22394  tsmsgsum  24168  rrxcph  25445  rrxfsupp  25455  mdegldg  26125  mdegcl  26128  plypf1  26271  fsuppinisegfi  32699  fsupprnfi  32704  fsuppcurry1  32739  fsuppcurry2  32740  offinsupp1  32741  gsumhashmul  33040  rmfsupp2  33218  elrspunidl  33421  elrspunsn  33422  rprmdvdsprod  33527  fedgmullem1  33642  fedgmullem2  33643  evls1fldgencl  33680  zarcmplem  33827  fsuppind  42545  mnringmulrcld  44197  rmfsupp  48099  mndpfsupp  48101  scmfsupp  48103  lincresunit2  48207