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	$$⊢\mathrm{Rel}\mathrm{finSupp}$$

Proof

Step	Hyp	Ref	Expression
1		df-fsupp	$$⊢\mathrm{finSupp}=\left\{⟨r,z⟩|\left(\mathrm{Fun}r\wedge r\mathrm{supp}z\in \mathrm{Fin}\right)\right\}$$
2	1	relopabi	$$⊢\mathrm{Rel}\mathrm{finSupp}$$