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 8317
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 8316 . 2 class finSupp
2 vr . . . . . 6 setvar 𝑟
32cv 1522 . . . . 5 class 𝑟
43wfun 5920 . . . 4 wff Fun 𝑟
5 vz . . . . . . 7 setvar 𝑧
65cv 1522 . . . . . 6 class 𝑧
7 csupp 7340 . . . . . 6 class supp
83, 6, 7co 6690 . . . . 5 class (𝑟 supp 𝑧)
9 cfn 7997 . . . . 5 class Fin
108, 9wcel 2030 . . . 4 wff (𝑟 supp 𝑧) ∈ Fin
114, 10wa 383 . . 3 wff (Fun 𝑟 ∧ (𝑟 supp 𝑧) ∈ Fin)
1211, 2, 5copab 4745 . 2 class {⟨𝑟, 𝑧⟩ ∣ (Fun 𝑟 ∧ (𝑟 supp 𝑧) ∈ Fin)}
131, 12wceq 1523 1 wff finSupp = {⟨𝑟, 𝑧⟩ ∣ (Fun 𝑟 ∧ (𝑟 supp 𝑧) ∈ Fin)}
Colors of variables: wff setvar class
This definition is referenced by:  relfsupp  8318  isfsupp  8320
  Copyright terms: Public domain W3C validator