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

Theorem isfsupp 9405
Description: The property of a class to be a finitely supported function (in relation to a given zero). (Contributed by AV, 23-May-2019.)
Assertion
Ref Expression
isfsupp ((𝑅𝑉𝑍𝑊) → (𝑅 finSupp 𝑍 ↔ (Fun 𝑅 ∧ (𝑅 supp 𝑍) ∈ Fin)))

Proof of Theorem isfsupp
Dummy variables 𝑟 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 funeq 6578 . . . 4 (𝑟 = 𝑅 → (Fun 𝑟 ↔ Fun 𝑅))
21adantr 479 . . 3 ((𝑟 = 𝑅𝑧 = 𝑍) → (Fun 𝑟 ↔ Fun 𝑅))
3 oveq12 7432 . . . 4 ((𝑟 = 𝑅𝑧 = 𝑍) → (𝑟 supp 𝑧) = (𝑅 supp 𝑍))
43eleq1d 2810 . . 3 ((𝑟 = 𝑅𝑧 = 𝑍) → ((𝑟 supp 𝑧) ∈ Fin ↔ (𝑅 supp 𝑍) ∈ Fin))
52, 4anbi12d 630 . 2 ((𝑟 = 𝑅𝑧 = 𝑍) → ((Fun 𝑟 ∧ (𝑟 supp 𝑧) ∈ Fin) ↔ (Fun 𝑅 ∧ (𝑅 supp 𝑍) ∈ Fin)))
6 df-fsupp 9402 . 2 finSupp = {⟨𝑟, 𝑧⟩ ∣ (Fun 𝑟 ∧ (𝑟 supp 𝑧) ∈ Fin)}
75, 6brabga 5539 1 ((𝑅𝑉𝑍𝑊) → (𝑅 finSupp 𝑍 ↔ (Fun 𝑅 ∧ (𝑅 supp 𝑍) ∈ Fin)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394   = wceq 1533  wcel 2098   class class class wbr 5152  Fun wfun 6547  (class class class)co 7423   supp csupp 8173  Fincfn 8973   finSupp cfsupp 9401
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696  ax-sep 5303  ax-nul 5310  ax-pr 5432
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-rab 3419  df-v 3463  df-dif 3949  df-un 3951  df-ss 3963  df-nul 4325  df-if 4533  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-br 5153  df-opab 5215  df-rel 5688  df-cnv 5689  df-co 5690  df-iota 6505  df-fun 6555  df-fv 6561  df-ov 7426  df-fsupp 9402
This theorem is referenced by:  isfsuppd  9406  funisfsupp  9407  fsuppimp  9408  fdmfifsupp  9414  fczfsuppd  9425  fsuppmptif  9438  fsuppco2  9442  fsuppcor  9443  gsumzadd  19915  gsumpt  19955  gsum2dlem2  19964  gsum2d  19965  gsum2d2lem  19966  mhpmulcl  22135  rmfsupp2  33080  elrspunidl  33280  naddcnff  42965  rmfsupp  47690  mndpfsupp  47692  scmfsupp  47694  mptcfsupp  47696
  Copyright terms: Public domain W3C validator