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 = { ⟨ 𝑟 , 𝑧 ⟩ ∣ ( Fun 𝑟 ∧ ( 𝑟 supp 𝑧 ) ∈ Fin ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfsupp	⊢ finSupp
1		vr	⊢ 𝑟
2		vz	⊢ 𝑧
3	1	cv	⊢ 𝑟
4	3	wfun	⊢ Fun 𝑟
5		csupp	⊢ supp
6	2	cv	⊢ 𝑧
7	3 6 5	co	⊢ ( 𝑟 supp 𝑧 )
8		cfn	⊢ Fin
9	7 8	wcel	⊢ ( 𝑟 supp 𝑧 ) ∈ Fin
10	4 9	wa	⊢ ( Fun 𝑟 ∧ ( 𝑟 supp 𝑧 ) ∈ Fin )
11	10 1 2	copab	⊢ { ⟨ 𝑟 , 𝑧 ⟩ ∣ ( Fun 𝑟 ∧ ( 𝑟 supp 𝑧 ) ∈ Fin ) }
12	0 11	wceq	⊢ finSupp = { ⟨ 𝑟 , 𝑧 ⟩ ∣ ( Fun 𝑟 ∧ ( 𝑟 supp 𝑧 ) ∈ Fin ) }