MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fsuppimpd Structured version   Visualization version   GIF version

Theorem fsuppimpd 8818
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
StepHypRef Expression
1 fsuppimpd.f . 2 (𝜑𝐹 finSupp 𝑍)
2 fsuppimp 8817 . . 3 (𝐹 finSupp 𝑍 → (Fun 𝐹 ∧ (𝐹 supp 𝑍) ∈ Fin))
32simprd 498 . 2 (𝐹 finSupp 𝑍 → (𝐹 supp 𝑍) ∈ Fin)
41, 3syl 17 1 (𝜑 → (𝐹 supp 𝑍) ∈ Fin)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2114   class class class wbr 5042  Fun wfun 6325  (class class class)co 7133   supp csupp 7808  Fincfn 8487   finSupp cfsupp 8811
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-sep 5179  ax-nul 5186  ax-pr 5306
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ral 3130  df-rex 3131  df-rab 3134  df-v 3475  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4270  df-if 4444  df-sn 4544  df-pr 4546  df-op 4550  df-uni 4815  df-br 5043  df-opab 5105  df-xp 5537  df-rel 5538  df-cnv 5539  df-co 5540  df-iota 6290  df-fun 6333  df-fv 6339  df-ov 7136  df-fsupp 8812
This theorem is referenced by:  fsuppsssupp  8827  fsuppxpfi  8828  fsuppun  8830  resfsupp  8838  fsuppmptif  8841  fsuppco  8843  fsuppco2  8844  fsuppcor  8845  cantnfcl  9108  cantnfp1lem1  9119  fsuppmapnn0fiublem  13342  fsuppmapnn0fiub  13343  fsuppmapnn0ub  13347  gsumzcl  19010  gsumcl  19014  gsumzadd  19021  gsumzmhm  19036  gsumzoppg  19043  gsum2dlem1  19069  gsum2dlem2  19070  gsum2d  19071  gsumxp2  19079  gsumdixp  19338  lcomfsupp  19650  mptscmfsupp0  19675  mplcoe1  20222  mplbas2  20227  psrbagev1  20266  evlslem2  20268  evlslem6  20270  regsumsupp  20742  frlmphllem  20900  uvcresum  20913  frlmsslsp  20916  frlmup1  20918  tsmsgsum  22723  rrxcph  23975  rrxfsupp  23985  mdegldg  24646  mdegcl  24649  plypf1  24788  fsuppcurry1  30448  fsuppcurry2  30449  offinsupp1  30450  rmfsupp2  30874  fedgmullem1  31036  fedgmullem2  31037  mnringmulrcld  40719  rmfsupp  44567  mndpfsupp  44569  scmfsupp  44571  lincresunit2  44678
  Copyright terms: Public domain W3C validator