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

Definition df-fsupp 8831
 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 8830 . 2 class finSupp
2 vr . . . . . 6 setvar 𝑟
32cv 1537 . . . . 5 class 𝑟
43wfun 6337 . . . 4 wff Fun 𝑟
5 vz . . . . . . 7 setvar 𝑧
65cv 1537 . . . . . 6 class 𝑧
7 csupp 7826 . . . . . 6 class supp
83, 6, 7co 7149 . . . . 5 class (𝑟 supp 𝑧)
9 cfn 8505 . . . . 5 class Fin
108, 9wcel 2115 . . . 4 wff (𝑟 supp 𝑧) ∈ Fin
114, 10wa 399 . . 3 wff (Fun 𝑟 ∧ (𝑟 supp 𝑧) ∈ Fin)
1211, 2, 5copab 5114 . 2 class {⟨𝑟, 𝑧⟩ ∣ (Fun 𝑟 ∧ (𝑟 supp 𝑧) ∈ Fin)}
131, 12wceq 1538 1 wff finSupp = {⟨𝑟, 𝑧⟩ ∣ (Fun 𝑟 ∧ (𝑟 supp 𝑧) ∈ Fin)}
 Colors of variables: wff setvar class This definition is referenced by:  relfsupp  8832  isfsupp  8834
 Copyright terms: Public domain W3C validator