Theorem fsuppimpd 9326

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 9325	. . 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 5109  Fun wfun 6507  (class class class)co 7389   supp csupp 8141  Fincfn 8920   finSupp cfsupp 9318

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 5253  ax-nul 5263  ax-pr 5389

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 3919  df-un 3921  df-ss 3933  df-nul 4299  df-if 4491  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5110  df-opab 5172  df-xp 5646  df-rel 5647  df-cnv 5648  df-co 5649  df-iota 6466  df-fun 6515  df-fv 6521  df-ov 7392  df-fsupp 9319

This theorem is referenced by:  fsuppsssupp  9338  fsuppsssuppgd  9339  fsuppxpfi  9342  fsuppun  9344  resfsupp  9353  fsuppmptif  9356  fsuppco  9359  fsuppco2  9360  fsuppcor  9361  cantnfcl  9626  cantnfp1lem1  9637  fsuppmapnn0fiublem  13961  fsuppmapnn0fiub  13962  fsuppmapnn0ub  13966  mndpfsupp  18700  gsumzcl  19847  gsumcl  19851  gsumzadd  19858  gsumzmhm  19873  gsumzoppg  19880  gsum2dlem1  19906  gsum2dlem2  19907  gsum2d  19908  gsumxp2  19916  gsumdixp  20234  lcomfsupp  20814  mptscmfsupp0  20839  regsumsupp  21537  frlmphllem  21695  uvcresum  21708  frlmsslsp  21711  frlmup1  21713  mplcoe1  21950  mplbas2  21955  psrbagev1  21990  evlslem2  21992  evlslem6  21994  psdmplcl  22055  evls1fpws  22262  tsmsgsum  24032  rrxcph  25298  rrxfsupp  25308  mdegldg  25977  mdegcl  25980  plypf1  26123  fsuppinisegfi  32616  fsupprnfi  32621  fsuppcurry1  32654  fsuppcurry2  32655  offinsupp1  32656  gsumfs2d  33001  gsumhashmul  33007  rmfsupp2  33195  elrgspnlem2  33200  elrgspnlem4  33202  elrgspnsubrunlem1  33204  elrgspnsubrunlem2  33205  elrspunidl  33405  elrspunsn  33406  rprmdvdsprod  33511  fedgmullem1  33631  fedgmullem2  33632  evls1fldgencl  33671  fldextrspunlsplem  33674  fldextrspunlsp  33675  zarcmplem  33877  fsuppind  42571  mnringmulrcld  44210  rmfsupp  48351  scmfsupp  48353  lincresunit2  48457