This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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$

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