Theorem fsuppimpd 9330

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

Syntax hints:   → wi 4   ∈ wcel 2143   class class class wbr 5110  Fun wfun 6532  (class class class)co 7412   supp csupp 8157  Fincfn 8944   finSupp cfsupp 9322

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-iota 6494  df-fun 6540  df-fv 6546  df-ov 7415  df-fsupp 9323

This theorem is referenced by:  fsuppsssupp  9342  fsuppsssuppgd  9343  fsuppxpfi  9346  fsuppun  9348  resfsupp  9357  fsuppmptif  9360  fsuppco  9363  fsuppco2  9364  fsuppcor  9365  cantnfcl  9637  cantnfp1lem1  9648  fsuppmapnn0fiublem  14028  fsuppmapnn0fiub  14029  fsuppmapnn0ub  14033  mndpfsupp  18826  gsumzcl  19982  gsumcl  19986  gsumzadd  19993  gsumzmhm  20008  gsumzoppg  20015  gsum2dlem1  20041  gsum2dlem2  20042  gsum2d  20043  gsumxp2  20051  gsumdixp  20401  lcomfsupp  21004  mptscmfsupp0  21029  regsumsupp  21753  frlmphllem  21911  uvcresum  21924  frlmsslsp  21927  frlmup1  21929  mplcoe1  22169  mplbas2  22174  psrbagev1  22209  evlslem2  22211  evlslem6  22213  psdmplcl  22306  evls1fpws  22510  tsmsgsum  24277  rrxcph  25532  rrxfsupp  25542  mdegldg  26204  mdegcl  26207  plypf1  26350  fsuppinisegfi  33010  fsupprnfi  33015  fsuppcurry1  33047  fsuppcurry2  33048  offinsupp1  33049  gsumfs2d  33359  gsumhashmul  33365  rmfsupp2  33535  elrgspnlem2  33541  elrgspnlem4  33543  elrgspnsubrunlem1  33545  elrgspnsubrunlem2  33546  elrspunidl  33714  elrspunsn  33715  rprmdvdsprod  33802  extvfvcl  33904  psrmonprod  33920  esplyfval3  33940  esplyind  33943  fedgmullem1  33997  fedgmullem2  33998  evls1fldgencl  34038  fldextrspunlsplem  34041  fldextrspunlsp  34042  zarcmplem  34249  fsuppind  43302  mnringmulrcld  44932  rmfsupp  49130  scmfsupp  49132  lincresunit2  49235