Definition df-fsupp 7819

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 = { <. r , z >. | ( Fun r /\ ( r supp z ) e. Fin ) }

Distinct variable group:   z, r

Detailed syntax breakdown of Definition df-fsupp

Step	Hyp	Ref	Expression
1		cfsupp 7818	. 2 class finSupp
2		vr	. . . . . 6 setvar r
3	2	cv 1373	. . . . 5 class r
4	3	wfun 5573	. . . 4 wff Fun r
5		vz	. . . . . . 7 setvar z
6	5	cv 1373	. . . . . 6 class z
7		csupp 6891	. . . . . 6 class supp
8	3, 6, 7	co 6275	. . . . 5 class ( r supp z )
9		cfn 7506	. . . . 5 class Fin
10	8, 9	wcel 1762	. . . 4 wff ( r supp z ) e. Fin
11	4, 10	wa 369	. . 3 wff ( Fun r /\ ( r supp z ) e. Fin )
12	11, 2, 5	copab 4497	. 2 class { <. r , z >. | ( Fun r /\ ( r supp z ) e. Fin ) }
13	1, 12	wceq 1374	1 wff finSupp = { <. r , z >. | ( Fun r /\ ( r supp z ) e. Fin ) }

This definition is referenced by:  relfsupp  7820  isfsupp  7822  fsuppimp  7824  wemapso2  7968