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

Theorem funisfsupp 8830
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 8829 . . 3 ((𝑅𝑉𝑍𝑊) → (𝑅 finSupp 𝑍 ↔ (Fun 𝑅 ∧ (𝑅 supp 𝑍) ∈ Fin)))
213adant1 1125 . 2 ((Fun 𝑅𝑅𝑉𝑍𝑊) → (𝑅 finSupp 𝑍 ↔ (Fun 𝑅 ∧ (𝑅 supp 𝑍) ∈ Fin)))
3 ibar 531 . . . 4 (Fun 𝑅 → ((𝑅 supp 𝑍) ∈ Fin ↔ (Fun 𝑅 ∧ (𝑅 supp 𝑍) ∈ Fin)))
43bicomd 225 . . 3 (Fun 𝑅 → ((Fun 𝑅 ∧ (𝑅 supp 𝑍) ∈ Fin) ↔ (𝑅 supp 𝑍) ∈ Fin))
543ad2ant1 1128 . 2 ((Fun 𝑅𝑅𝑉𝑍𝑊) → ((Fun 𝑅 ∧ (𝑅 supp 𝑍) ∈ Fin) ↔ (𝑅 supp 𝑍) ∈ Fin))
62, 5bitrd 281 1 ((Fun 𝑅𝑅𝑉𝑍𝑊) → (𝑅 finSupp 𝑍 ↔ (𝑅 supp 𝑍) ∈ Fin))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wa 398  w3a 1082  wcel 2108   class class class wbr 5057  Fun wfun 6342  (class class class)co 7148   supp csupp 7822  Fincfn 8501   finSupp cfsupp 8825
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pr 5320
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-rex 3142  df-rab 3145  df-v 3495  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-opab 5120  df-rel 5555  df-cnv 5556  df-co 5557  df-iota 6307  df-fun 6350  df-fv 6356  df-ov 7151  df-fsupp 8826
This theorem is referenced by:  suppeqfsuppbi  8839  suppssfifsupp  8840  fsuppunbi  8846  0fsupp  8847  snopfsupp  8848  fsuppres  8850  resfsupp  8852  frnfsuppbi  8854  fsuppco  8857  sniffsupp  8865  cantnfp1lem1  9133  mptnn0fsupp  13357  dprdfadd  19134  lcomfsupp  19666  mplsubglem2  20208  ltbwe  20245  frlmbas  20891  frlmphllem  20916  frlmsslsp  20932  pmatcollpw2lem  21377  rrxmval  24000  offinsupp1  30455  eulerpartgbij  31623  pwfi2f1o  39687  fidmfisupp  41452  lcoc0  44468
  Copyright terms: Public domain W3C validator