Definition df-fsupp 9129

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

Step	Hyp	Ref	Expression
1		cfsupp 9128	. 2 class finSupp
2		vr	. . . . . 6 setvar 𝑟
3	2	cv 1538	. . . . 5 class 𝑟
4	3	wfun 6427	. . . 4 wff Fun 𝑟
5		vz	. . . . . . 7 setvar 𝑧
6	5	cv 1538	. . . . . 6 class 𝑧
7		csupp 7977	. . . . . 6 class supp
8	3, 6, 7	co 7275	. . . . 5 class (𝑟 supp 𝑧)
9		cfn 8733	. . . . 5 class Fin
10	8, 9	wcel 2106	. . . 4 wff (𝑟 supp 𝑧) ∈ Fin
11	4, 10	wa 396	. . 3 wff (Fun 𝑟 ∧ (𝑟 supp 𝑧) ∈ Fin)
12	11, 2, 5	copab 5136	. 2 class {⟨𝑟, 𝑧⟩ ∣ (Fun 𝑟 ∧ (𝑟 supp 𝑧) ∈ Fin)}
13	1, 12	wceq 1539	1 wff finSupp = {⟨𝑟, 𝑧⟩ ∣ (Fun 𝑟 ∧ (𝑟 supp 𝑧) ∈ Fin)}

This definition is referenced by:  relfsupp  9130  isfsupp  9132