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

Theorem funisfsupp 8884
 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 𝑅𝑅𝑉𝑍𝑊) → (𝑅 finSupp 𝑍 ↔ (𝑅 supp 𝑍) ∈ Fin))

Proof of Theorem funisfsupp
StepHypRef Expression
1 isfsupp 8883 . . 3 ((𝑅𝑉𝑍𝑊) → (𝑅 finSupp 𝑍 ↔ (Fun 𝑅 ∧ (𝑅 supp 𝑍) ∈ Fin)))
213adant1 1127 . 2 ((Fun 𝑅𝑅𝑉𝑍𝑊) → (𝑅 finSupp 𝑍 ↔ (Fun 𝑅 ∧ (𝑅 supp 𝑍) ∈ Fin)))
3 ibar 532 . . . 4 (Fun 𝑅 → ((𝑅 supp 𝑍) ∈ Fin ↔ (Fun 𝑅 ∧ (𝑅 supp 𝑍) ∈ Fin)))
43bicomd 226 . . 3 (Fun 𝑅 → ((Fun 𝑅 ∧ (𝑅 supp 𝑍) ∈ Fin) ↔ (𝑅 supp 𝑍) ∈ Fin))
543ad2ant1 1130 . 2 ((Fun 𝑅𝑅𝑉𝑍𝑊) → ((Fun 𝑅 ∧ (𝑅 supp 𝑍) ∈ Fin) ↔ (𝑅 supp 𝑍) ∈ Fin))
62, 5bitrd 282 1 ((Fun 𝑅𝑅𝑉𝑍𝑊) → (𝑅 finSupp 𝑍 ↔ (𝑅 supp 𝑍) ∈ Fin))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   ∈ wcel 2111   class class class wbr 5036  Fun wfun 6334  (class class class)co 7156   supp csupp 7841  Fincfn 8540   finSupp cfsupp 8879 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729  ax-sep 5173  ax-nul 5180  ax-pr 5302 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-nul 4228  df-if 4424  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-br 5037  df-opab 5099  df-rel 5535  df-cnv 5536  df-co 5537  df-iota 6299  df-fun 6342  df-fv 6348  df-ov 7159  df-fsupp 8880 This theorem is referenced by:  suppeqfsuppbi  8893  suppssfifsupp  8894  fsuppunbi  8900  0fsupp  8901  snopfsupp  8902  fsuppres  8904  resfsupp  8906  frnfsuppbi  8908  sniffsupp  8910  fsuppco  8912  cantnfp1lem1  9187  frnnn0fsuppg  12006  mptnn0fsupp  13427  dprdfadd  19223  lcomfsupp  19755  frlmbas  20533  frlmphllem  20558  frlmsslsp  20574  mplsubglem2  20779  ltbwe  20817  pmatcollpw2lem  21490  rrxmval  24118  offinsupp1  30598  elrspunidl  31139  eulerpartgbij  31870  pwfi2f1o  40448  finnzfsuppd  41323  fidmfisupp  42233  lcoc0  45245
 Copyright terms: Public domain W3C validator