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 ( R supp Z ) e. 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 = { <. r , z >. | ( Fun r /\ E. w ( w e. Fin /\ w C_ dom r /\ ( r " ( dom r \ w ) ) C_ { z } ) ) }

Distinct variable group:   w, r, z

Detailed syntax breakdown of Definition df-fsuppfi

Step	Hyp	Ref	Expression
1		cfsupp 7292	. 2 class finSupp
2		vr	. . . . . 6 setvar r
3	2	cv 1401	. . . . 5 class r
4	3	wfun 5374	. . . 4 wff Fun r
5		vw	. . . . . . . 8 setvar w
6	5	cv 1401	. . . . . . 7 class w
7		cfn 7028	. . . . . . 7 class Fin
8	6, 7	wcel 2209	. . . . . 6 wff w e. Fin
9	3	cdm 4776	. . . . . . 7 class dom r
10	6, 9	wss 3220	. . . . . 6 wff w C_ dom r
11	9, 6	cdif 3217	. . . . . . . 8 class ( dom r \ w )
12	3, 11	cima 4779	. . . . . . 7 class ( r " ( dom r \ w ) )
13		vz	. . . . . . . . 9 setvar z
14	13	cv 1401	. . . . . . . 8 class z
15	14	csn 3709	. . . . . . 7 class { z }
16	12, 15	wss 3220	. . . . . 6 wff ( r " ( dom r \ w ) ) C_ { z }
17	8, 10, 16	w3a 1009	. . . . 5 wff ( w e. Fin /\ w C_ dom r /\ ( r " ( dom r \ w ) ) C_ { z } )
18	17, 5	wex 1545	. . . 4 wff E. w ( w e. Fin /\ w C_ dom r /\ ( r " ( dom r \ w ) ) C_ { z } )
19	4, 18	wa 104	. . 3 wff ( Fun r /\ E. w ( w e. Fin /\ w C_ dom r /\ ( r " ( dom r \ w ) ) C_ { z } ) )
20	19, 2, 13	copab 4192	. 2 class { <. r , z >. | ( Fun r /\ E. w ( w e. Fin /\ w C_ dom r /\ ( r " ( dom r \ w ) ) C_ { z } ) ) }
21	1, 20	wceq 1402	1 wff finSupp = { <. r , z >. | ( Fun r /\ E. w ( w e. Fin /\ w C_ dom r /\ ( r " ( dom r \ w ) ) C_ { z } ) ) }

This definition is used by:  relfsupp  7294  isfsuppfi  7296