Definition df-fsuppfi 7293

Description: Define the property of a function to be finitely supported (in relation to a given zero). This definition will perhaps be most useful when the domain of the function has decidable equality; consider as an alternative (𝑅 supp 𝑍) ∈ Fin (see df-supp 6480) which will behave well when a codomain of the function has decidable equality. If both domain and codomain have decidable equality, the two are equivalent as seen at funisfsuppdc 7298. (Contributed by AV, 23-May-2019.) (Revised by Jim Kingdon, 16-Oct-2026.)

Assertion

Ref	Expression
df-fsuppfi	⊢ finSupp = {⟨𝑟, 𝑧⟩ ∣ (Fun 𝑟 ∧ ∃𝑤(𝑤 ∈ Fin ∧ 𝑤 ⊆ dom 𝑟 ∧ (𝑟 “ (dom 𝑟 ∖ 𝑤)) ⊆ {𝑧}))}

Distinct variable group:   𝑤,𝑟,𝑧

Detailed syntax breakdown of Definition df-fsuppfi

Step	Hyp	Ref	Expression
1		cfsupp 7292	. 2 class finSupp
2		vr	. . . . . 6 setvar 𝑟
3	2	cv 1401	. . . . 5 class 𝑟
4	3	wfun 5374	. . . 4 wff Fun 𝑟
5		vw	. . . . . . . 8 setvar 𝑤
6	5	cv 1401	. . . . . . 7 class 𝑤
7		cfn 7028	. . . . . . 7 class Fin
8	6, 7	wcel 2209	. . . . . 6 wff 𝑤 ∈ Fin
9	3	cdm 4776	. . . . . . 7 class dom 𝑟
10	6, 9	wss 3220	. . . . . 6 wff 𝑤 ⊆ dom 𝑟
11	9, 6	cdif 3217	. . . . . . . 8 class (dom 𝑟 ∖ 𝑤)
12	3, 11	cima 4779	. . . . . . 7 class (𝑟 “ (dom 𝑟 ∖ 𝑤))
13		vz	. . . . . . . . 9 setvar 𝑧
14	13	cv 1401	. . . . . . . 8 class 𝑧
15	14	csn 3709	. . . . . . 7 class {𝑧}
16	12, 15	wss 3220	. . . . . 6 wff (𝑟 “ (dom 𝑟 ∖ 𝑤)) ⊆ {𝑧}
17	8, 10, 16	w3a 1009	. . . . 5 wff (𝑤 ∈ Fin ∧ 𝑤 ⊆ dom 𝑟 ∧ (𝑟 “ (dom 𝑟 ∖ 𝑤)) ⊆ {𝑧})
18	17, 5	wex 1545	. . . 4 wff ∃𝑤(𝑤 ∈ Fin ∧ 𝑤 ⊆ dom 𝑟 ∧ (𝑟 “ (dom 𝑟 ∖ 𝑤)) ⊆ {𝑧})
19	4, 18	wa 104	. . 3 wff (Fun 𝑟 ∧ ∃𝑤(𝑤 ∈ Fin ∧ 𝑤 ⊆ dom 𝑟 ∧ (𝑟 “ (dom 𝑟 ∖ 𝑤)) ⊆ {𝑧}))
20	19, 2, 13	copab 4192	. 2 class {⟨𝑟, 𝑧⟩ ∣ (Fun 𝑟 ∧ ∃𝑤(𝑤 ∈ Fin ∧ 𝑤 ⊆ dom 𝑟 ∧ (𝑟 “ (dom 𝑟 ∖ 𝑤)) ⊆ {𝑧}))}
21	1, 20	wceq 1402	1 wff finSupp = {⟨𝑟, 𝑧⟩ ∣ (Fun 𝑟 ∧ ∃𝑤(𝑤 ∈ Fin ∧ 𝑤 ⊆ dom 𝑟 ∧ (𝑟 “ (dom 𝑟 ∖ 𝑤)) ⊆ {𝑧}))}

This definition is used by:  relfsupp  7294  isfsuppfi  7296