Theorem fsuppimpd 8906

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

Syntax hints:   → wi 4   ∈ wcel 2113   class class class wbr 5027  Fun wfun 6327  (class class class)co 7164   supp csupp 7849  Fincfn 8548   finSupp cfsupp 8899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710  ax-sep 5164  ax-nul 5171  ax-pr 5293

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-ral 3058  df-rex 3059  df-v 3399  df-dif 3844  df-un 3846  df-in 3848  df-ss 3858  df-nul 4210  df-if 4412  df-sn 4514  df-pr 4516  df-op 4520  df-uni 4794  df-br 5028  df-opab 5090  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-iota 6291  df-fun 6335  df-fv 6341  df-ov 7167  df-fsupp 8900

This theorem is referenced by:  fsuppsssupp  8915  fsuppxpfi  8916  fsuppun  8918  resfsupp  8926  fsuppmptif  8929  fsuppco  8932  fsuppco2  8933  fsuppcor  8934  cantnfcl  9196  cantnfp1lem1  9207  fsuppmapnn0fiublem  13442  fsuppmapnn0fiub  13443  fsuppmapnn0ub  13447  gsumzcl  19143  gsumcl  19147  gsumzadd  19154  gsumzmhm  19169  gsumzoppg  19176  gsum2dlem1  19202  gsum2dlem2  19203  gsum2d  19204  gsumxp2  19212  gsumdixp  19474  lcomfsupp  19786  mptscmfsupp0  19811  regsumsupp  20431  frlmphllem  20589  uvcresum  20602  frlmsslsp  20605  frlmup1  20607  mplcoe1  20841  mplbas2  20846  psrbagev1  20882  psrbagev1OLD  20883  evlslem2  20886  evlslem6  20888  tsmsgsum  22883  rrxcph  24137  rrxfsupp  24147  mdegldg  24811  mdegcl  24814  plypf1  24953  fsuppinisegfi  30588  fsupprnfi  30593  fsuppcurry1  30627  fsuppcurry2  30628  offinsupp1  30629  gsumhashmul  30885  rmfsupp2  31061  elrspunidl  31170  fedgmullem1  31274  fedgmullem2  31275  zarcmplem  31395  evlsbagval  39838  fsuppind  39842  mhphf  39848  mnringmulrcld  41372  rmfsupp  45228  mndpfsupp  45230  scmfsupp  45232  lincresunit2  45337