Theorem fsuppimpd 9327

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 9326	. . 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 2109   class class class wbr 5110  Fun wfun 6508  (class class class)co 7390   supp csupp 8142  Fincfn 8921   finSupp cfsupp 9319

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-iota 6467  df-fun 6516  df-fv 6522  df-ov 7393  df-fsupp 9320

This theorem is referenced by:  fsuppsssupp  9339  fsuppsssuppgd  9340  fsuppxpfi  9343  fsuppun  9345  resfsupp  9354  fsuppmptif  9357  fsuppco  9360  fsuppco2  9361  fsuppcor  9362  cantnfcl  9627  cantnfp1lem1  9638  fsuppmapnn0fiublem  13962  fsuppmapnn0fiub  13963  fsuppmapnn0ub  13967  mndpfsupp  18701  gsumzcl  19848  gsumcl  19852  gsumzadd  19859  gsumzmhm  19874  gsumzoppg  19881  gsum2dlem1  19907  gsum2dlem2  19908  gsum2d  19909  gsumxp2  19917  gsumdixp  20235  lcomfsupp  20815  mptscmfsupp0  20840  regsumsupp  21538  frlmphllem  21696  uvcresum  21709  frlmsslsp  21712  frlmup1  21714  mplcoe1  21951  mplbas2  21956  psrbagev1  21991  evlslem2  21993  evlslem6  21995  psdmplcl  22056  evls1fpws  22263  tsmsgsum  24033  rrxcph  25299  rrxfsupp  25309  mdegldg  25978  mdegcl  25981  plypf1  26124  fsuppinisegfi  32617  fsupprnfi  32622  fsuppcurry1  32655  fsuppcurry2  32656  offinsupp1  32657  gsumfs2d  33002  gsumhashmul  33008  rmfsupp2  33196  elrgspnlem2  33201  elrgspnlem4  33203  elrgspnsubrunlem1  33205  elrgspnsubrunlem2  33206  elrspunidl  33406  elrspunsn  33407  rprmdvdsprod  33512  fedgmullem1  33632  fedgmullem2  33633  evls1fldgencl  33672  fldextrspunlsplem  33675  fldextrspunlsp  33676  zarcmplem  33878  fsuppind  42585  mnringmulrcld  44224  rmfsupp  48365  scmfsupp  48367  lincresunit2  48471