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

Definition df-fsupp 8132
Description: Define the property of a function to be finitely supported (in relation to a given zero). (Contributed by AV, 23-May-2019.)
Assertion
Ref Expression
df-fsupp finSupp = {⟨𝑟, 𝑧⟩ ∣ (Fun 𝑟 ∧ (𝑟 supp 𝑧) ∈ Fin)}
Distinct variable group:   𝑧,𝑟

Detailed syntax breakdown of Definition df-fsupp
StepHypRef Expression
1 cfsupp 8131 . 2 class finSupp
2 vr . . . . . 6 setvar 𝑟
32cv 1473 . . . . 5 class 𝑟
43wfun 5780 . . . 4 wff Fun 𝑟
5 vz . . . . . . 7 setvar 𝑧
65cv 1473 . . . . . 6 class 𝑧
7 csupp 7155 . . . . . 6 class supp
83, 6, 7co 6523 . . . . 5 class (𝑟 supp 𝑧)
9 cfn 7814 . . . . 5 class Fin
108, 9wcel 1975 . . . 4 wff (𝑟 supp 𝑧) ∈ Fin
114, 10wa 382 . . 3 wff (Fun 𝑟 ∧ (𝑟 supp 𝑧) ∈ Fin)
1211, 2, 5copab 4632 . 2 class {⟨𝑟, 𝑧⟩ ∣ (Fun 𝑟 ∧ (𝑟 supp 𝑧) ∈ Fin)}
131, 12wceq 1474 1 wff finSupp = {⟨𝑟, 𝑧⟩ ∣ (Fun 𝑟 ∧ (𝑟 supp 𝑧) ∈ Fin)}
Colors of variables: wff setvar class
This definition is referenced by:  relfsupp  8133  isfsupp  8135
  Copyright terms: Public domain W3C validator