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

Theorem funisfsupp 7723
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  |-  ( ( Fun  R  /\  R  e.  V  /\  Z  e.  W )  ->  ( R finSupp  Z  <->  ( R supp  Z
)  e.  Fin )
)

Proof of Theorem funisfsupp
StepHypRef Expression
1 isfsupp 7722 . . 3  |-  ( ( R  e.  V  /\  Z  e.  W )  ->  ( R finSupp  Z  <->  ( Fun  R  /\  ( R supp  Z
)  e.  Fin )
) )
213adant1 1006 . 2  |-  ( ( Fun  R  /\  R  e.  V  /\  Z  e.  W )  ->  ( R finSupp  Z  <->  ( Fun  R  /\  ( R supp  Z )  e.  Fin ) ) )
3 ibar 504 . . . 4  |-  ( Fun 
R  ->  ( ( R supp  Z )  e.  Fin  <->  ( Fun  R  /\  ( R supp 
Z )  e.  Fin ) ) )
43bicomd 201 . . 3  |-  ( Fun 
R  ->  ( ( Fun  R  /\  ( R supp 
Z )  e.  Fin ) 
<->  ( R supp  Z )  e.  Fin ) )
543ad2ant1 1009 . 2  |-  ( ( Fun  R  /\  R  e.  V  /\  Z  e.  W )  ->  (
( Fun  R  /\  ( R supp  Z )  e.  Fin )  <->  ( R supp  Z )  e.  Fin )
)
62, 5bitrd 253 1  |-  ( ( Fun  R  /\  R  e.  V  /\  Z  e.  W )  ->  ( R finSupp  Z  <->  ( R supp  Z
)  e.  Fin )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 965    e. wcel 1758   class class class wbr 4387   Fun wfun 5507  (class class class)co 6187   supp csupp 6787   Fincfn 7407   finSupp cfsupp 7718
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4508  ax-nul 4516  ax-pr 4626
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2599  df-ne 2644  df-rex 2799  df-rab 2802  df-v 3067  df-dif 3426  df-un 3428  df-in 3430  df-ss 3437  df-nul 3733  df-if 3887  df-sn 3973  df-pr 3975  df-op 3979  df-uni 4187  df-br 4388  df-opab 4446  df-rel 4942  df-cnv 4943  df-co 4944  df-iota 5476  df-fun 5515  df-fv 5521  df-ov 6190  df-fsupp 7719
This theorem is referenced by:  suppeqfsuppbi  7732  suppssfifsupp  7733  fsuppunbi  7739  0fsupp  7740  snopfsupp  7741  fsuppres  7743  resfsupp  7745  frnfsuppbi  7746  fsuppco  7749  sniffsupp  7757  cantnffvalOLD  7969  cantnfp1lem1  7984  dprdvalOLD  16589  dprdfadd  16612  lcomfsupp  17088  mplsubglem2  17618  ltbwe  17658  frlmbas  18286  frlmphllem  18311  frlmsslsp  18329  rrxmval  21017  eulerpartgbij  26886  mptnn0fsupp  30937  lcoc0  31060  pmatcollpwlem  31230
  Copyright terms: Public domain W3C validator