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 \land r supp z \in Fin)\}$

Step	Hyp	Ref	Expression
0		cfsupp	$class finSupp$
1		vr	$setvar r$
2		vz	$setvar z$
3	1	cv	$setvar r$
4	3	wfun	$wff Fun r$
5		csupp	$class supp$
6	2	cv	$setvar z$
7	3 6 5	co	$class {supp}_{z} (r)$
8		cfn	$class Fin$
9	7 8	wcel	$wff r supp z \in Fin$
10	4 9	wa	$wff (Fun r \land r supp z \in Fin)$
11	10 1 2	copab	$class \{⟨r, z⟩ \| (Fun r \land r supp z \in Fin)\}$
12	0 11	wceq	$wff finSupp = \{⟨r, z⟩ \| (Fun r \land r supp z \in Fin)\}$

Metamath Proof Explorer