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

Theorem funisfsupp 8163
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 8162 . . 3 ((𝑅𝑉𝑍𝑊) → (𝑅 finSupp 𝑍 ↔ (Fun 𝑅 ∧ (𝑅 supp 𝑍) ∈ Fin)))
213adant1 1072 . 2 ((Fun 𝑅𝑅𝑉𝑍𝑊) → (𝑅 finSupp 𝑍 ↔ (Fun 𝑅 ∧ (𝑅 supp 𝑍) ∈ Fin)))
3 ibar 524 . . . 4 (Fun 𝑅 → ((𝑅 supp 𝑍) ∈ Fin ↔ (Fun 𝑅 ∧ (𝑅 supp 𝑍) ∈ Fin)))
43bicomd 212 . . 3 (Fun 𝑅 → ((Fun 𝑅 ∧ (𝑅 supp 𝑍) ∈ Fin) ↔ (𝑅 supp 𝑍) ∈ Fin))
543ad2ant1 1075 . 2 ((Fun 𝑅𝑅𝑉𝑍𝑊) → ((Fun 𝑅 ∧ (𝑅 supp 𝑍) ∈ Fin) ↔ (𝑅 supp 𝑍) ∈ Fin))
62, 5bitrd 267 1 ((Fun 𝑅𝑅𝑉𝑍𝑊) → (𝑅 finSupp 𝑍 ↔ (𝑅 supp 𝑍) ∈ Fin))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wa 383  w3a 1031  wcel 1977   class class class wbr 4583  Fun wfun 5798  (class class class)co 6549   supp csupp 7182  Fincfn 7841   finSupp cfsupp 8158
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-rel 5045  df-cnv 5046  df-co 5047  df-iota 5768  df-fun 5806  df-fv 5812  df-ov 6552  df-fsupp 8159
This theorem is referenced by:  suppeqfsuppbi  8172  suppssfifsupp  8173  fsuppunbi  8179  0fsupp  8180  snopfsupp  8181  fsuppres  8183  resfsupp  8185  frnfsuppbi  8187  fsuppco  8190  sniffsupp  8198  cantnfp1lem1  8458  mptnn0fsupp  12659  dprdfadd  18242  lcomfsupp  18726  mplsubglem2  19257  ltbwe  19293  frlmbas  19918  frlmphllem  19938  frlmsslsp  19954  pmatcollpw2lem  20401  rrxmval  22996  eulerpartgbij  29761  pwfi2f1o  36684  fidmfisupp  38385  lcoc0  42005
  Copyright terms: Public domain W3C validator