Definition df-fsupp

Description: Define the property of a function to be finitely supported (in relation to a given zero). (Contributed by AV, 23-May-2019)

	Ref	Expression
Assertion	df-fsupp	|- finSupp = { <. r , z >. | ( Fun r /\ ( r supp z ) e. Fin ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfsupp	|- finSupp
1		vr	|- r
2		vz	|- z
3	1	cv	|- r
4	3	wfun	|- Fun r
5		csupp	|- supp
6	2	cv	|- z
7	3 6 5	co	|- ( r supp z )
8		cfn	|- Fin
9	7 8	wcel	|- ( r supp z ) e. Fin
10	4 9	wa	|- ( Fun r /\ ( r supp z ) e. Fin )
11	10 1 2	copab	|- { <. r , z >. | ( Fun r /\ ( r supp z ) e. Fin ) }
12	0 11	wceq	|- finSupp = { <. r , z >. | ( Fun r /\ ( r supp z ) e. Fin ) }