Theorem relfsupp

Description: The property of a function to be finitely supported is a relation. (Contributed by AV, 7-Jun-2019)

	Ref	Expression
Assertion	relfsupp	⊢ Rel finSupp

Proof

Step	Hyp	Ref	Expression
1		df-fsupp	⊢ finSupp = { ⟨ 𝑟 , 𝑧 ⟩ ∣ ( Fun 𝑟 ∧ ( 𝑟 supp 𝑧 ) ∈ Fin ) }
2	1	relopabiv	⊢ Rel finSupp