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 9099
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 9098 . 2 class finSupp
2 vr . . . . . 6 setvar 𝑟
32cv 1541 . . . . 5 class 𝑟
43wfun 6425 . . . 4 wff Fun 𝑟
5 vz . . . . . . 7 setvar 𝑧
65cv 1541 . . . . . 6 class 𝑧
7 csupp 7962 . . . . . 6 class supp
83, 6, 7co 7269 . . . . 5 class (𝑟 supp 𝑧)
9 cfn 8708 . . . . 5 class Fin
108, 9wcel 2110 . . . 4 wff (𝑟 supp 𝑧) ∈ Fin
114, 10wa 396 . . 3 wff (Fun 𝑟 ∧ (𝑟 supp 𝑧) ∈ Fin)
1211, 2, 5copab 5141 . 2 class {⟨𝑟, 𝑧⟩ ∣ (Fun 𝑟 ∧ (𝑟 supp 𝑧) ∈ Fin)}
131, 12wceq 1542 1 wff finSupp = {⟨𝑟, 𝑧⟩ ∣ (Fun 𝑟 ∧ (𝑟 supp 𝑧) ∈ Fin)}
Colors of variables: wff setvar class
This definition is referenced by:  relfsupp  9100  isfsupp  9102
  Copyright terms: Public domain W3C validator