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

Theorem isfsupp 9402
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 6587 . . . 4 (𝑟 = 𝑅 → (Fun 𝑟 ↔ Fun 𝑅))
21adantr 480 . . 3 ((𝑟 = 𝑅𝑧 = 𝑍) → (Fun 𝑟 ↔ Fun 𝑅))
3 oveq12 7439 . . . 4 ((𝑟 = 𝑅𝑧 = 𝑍) → (𝑟 supp 𝑧) = (𝑅 supp 𝑍))
43eleq1d 2823 . . 3 ((𝑟 = 𝑅𝑧 = 𝑍) → ((𝑟 supp 𝑧) ∈ Fin ↔ (𝑅 supp 𝑍) ∈ Fin))
52, 4anbi12d 632 . 2 ((𝑟 = 𝑅𝑧 = 𝑍) → ((Fun 𝑟 ∧ (𝑟 supp 𝑧) ∈ Fin) ↔ (Fun 𝑅 ∧ (𝑅 supp 𝑍) ∈ Fin)))
6 df-fsupp 9399 . 2 finSupp = {⟨𝑟, 𝑧⟩ ∣ (Fun 𝑟 ∧ (𝑟 supp 𝑧) ∈ Fin)}
75, 6brabga 5543 1 ((𝑅𝑉𝑍𝑊) → (𝑅 finSupp 𝑍 ↔ (Fun 𝑅 ∧ (𝑅 supp 𝑍) ∈ Fin)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1536  wcel 2105   class class class wbr 5147  Fun wfun 6556  (class class class)co 7430   supp csupp 8183  Fincfn 8983   finSupp cfsupp 9398
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-rel 5695  df-cnv 5696  df-co 5697  df-iota 6515  df-fun 6564  df-fv 6570  df-ov 7433  df-fsupp 9399
This theorem is referenced by:  isfsuppd  9403  funisfsupp  9404  fsuppimp  9405  fdmfifsupp  9412  fczfsuppd  9423  fsuppmptif  9436  fsuppco2  9440  fsuppcor  9441  mndpfsupp  18792  gsumzadd  19954  gsumpt  19994  gsum2dlem2  20003  gsum2d  20004  gsum2d2lem  20005  mhpmulcl  22170  rmfsupp2  33227  elrspunidl  33435  naddcnff  43351  rmfsupp  48217  scmfsupp  48219  mptcfsupp  48221
  Copyright terms: Public domain W3C validator