Definition df-supp 6470

Description: Define the support of a function against a "zero" value. The support of a function is the subset of its domain which is mapped to a value which is not equal to a designed value called the zero value. Note that this definition uses not equal rather than being in terms of an apartness relation (df-ap 8904 or any other apartness relation), and thus is sometimes called "support" rather than "strong support". It is therefore probably most useful when the function has a codomain which has decidable equality and contains the zero value. (Contributed by AV, 31-Mar-2019.) (Revised by AV, 6-Apr-2019.)

Assertion

Ref	Expression
df-supp	⊢ supp = (𝑥 ∈ V, 𝑧 ∈ V ↦ {𝑖 ∈ dom 𝑥 ∣ (𝑥 “ {𝑖}) ≠ {𝑧}})

Distinct variable group:   𝑥,𝑖,𝑧

Detailed syntax breakdown of Definition df-supp

Step	Hyp	Ref	Expression
1		csupp 6469	. 2 class supp
2		vx	. . 3 setvar 𝑥
3		vz	. . 3 setvar 𝑧
4		cvv 2821	. . 3 class V
5	2	cv 1401	. . . . . 6 class 𝑥
6		vi	. . . . . . . 8 setvar 𝑖
7	6	cv 1401	. . . . . . 7 class 𝑖
8	7	csn 3708	. . . . . 6 class {𝑖}
9	5, 8	cima 4775	. . . . 5 class (𝑥 “ {𝑖})
10	3	cv 1401	. . . . . 6 class 𝑧
11	10	csn 3708	. . . . 5 class {𝑧}
12	9, 11	wne 2420	. . . 4 wff (𝑥 “ {𝑖}) ≠ {𝑧}
13	5	cdm 4772	. . . 4 class dom 𝑥
14	12, 6, 13	crab 2532	. . 3 class {𝑖 ∈ dom 𝑥 ∣ (𝑥 “ {𝑖}) ≠ {𝑧}}
15	2, 3, 4, 4, 14	cmpo 6081	. 2 class (𝑥 ∈ V, 𝑧 ∈ V ↦ {𝑖 ∈ dom 𝑥 ∣ (𝑥 “ {𝑖}) ≠ {𝑧}})
16	1, 15	wceq 1402	1 wff supp = (𝑥 ∈ V, 𝑧 ∈ V ↦ {𝑖 ∈ dom 𝑥 ∣ (𝑥 “ {𝑖}) ≠ {𝑧}})

This definition is referenced by:  suppval  6471  funsssuppss  6492  fczsupp0  6493  suppssdc  6494  suppssfvg  6497  suppcofn  6500