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 8823
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 8822 . 2 class finSupp
2 vr . . . . . 6 setvar 𝑟
32cv 1527 . . . . 5 class 𝑟
43wfun 6343 . . . 4 wff Fun 𝑟
5 vz . . . . . . 7 setvar 𝑧
65cv 1527 . . . . . 6 class 𝑧
7 csupp 7821 . . . . . 6 class supp
83, 6, 7co 7145 . . . . 5 class (𝑟 supp 𝑧)
9 cfn 8498 . . . . 5 class Fin
108, 9wcel 2105 . . . 4 wff (𝑟 supp 𝑧) ∈ Fin
114, 10wa 396 . . 3 wff (Fun 𝑟 ∧ (𝑟 supp 𝑧) ∈ Fin)
1211, 2, 5copab 5120 . 2 class {⟨𝑟, 𝑧⟩ ∣ (Fun 𝑟 ∧ (𝑟 supp 𝑧) ∈ Fin)}
131, 12wceq 1528 1 wff finSupp = {⟨𝑟, 𝑧⟩ ∣ (Fun 𝑟 ∧ (𝑟 supp 𝑧) ∈ Fin)}
Colors of variables: wff setvar class
This definition is referenced by:  relfsupp  8824  isfsupp  8826
  Copyright terms: Public domain W3C validator