MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  funisfsupp Unicode version

Theorem funisfsupp 7854
Description: The property of a function to be finitely supported (in relation to a given zero). (Contributed by AV, 23-May-2019.)
Assertion
Ref Expression
funisfsupp

Proof of Theorem funisfsupp
StepHypRef Expression
1 isfsupp 7853 . . 3
213adant1 1014 . 2
3 ibar 504 . . . 4
43bicomd 201 . . 3
543ad2ant1 1017 . 2
62, 5bitrd 253 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  /\w3a 973  e.wcel 1818   class class class wbr 4452  Funwfun 5587  (class class class)co 6296   csupp 6918   cfn 7536   cfsupp 7849
This theorem is referenced by:  suppeqfsuppbi  7863  suppssfifsupp  7864  fsuppunbi  7870  0fsupp  7871  snopfsupp  7872  fsuppres  7874  resfsupp  7876  frnfsuppbi  7878  fsuppco  7881  sniffsupp  7889  cantnffvalOLD  8103  cantnfp1lem1  8118  mptnn0fsupp  12103  dprdvalOLD  17036  dprdfadd  17060  lcomfsupp  17550  mplsubglem2  18097  ltbwe  18137  frlmbas  18786  frlmphllem  18811  frlmsslsp  18829  pmatcollpw2lem  19278  rrxmval  21832  eulerpartgbij  28311  lcoc0  33023
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-rel 5011  df-cnv 5012  df-co 5013  df-iota 5556  df-fun 5595  df-fv 5601  df-ov 6299  df-fsupp 7850
  Copyright terms: Public domain W3C validator