isfsupp

Description: The property of a class to be a finitely supported function (in relation to a given zero). (Contributed by AV, 23-May-2019)

		Ref	Expression
	Assertion	isfsupp	$⊢ (R \in V \land Z \in W) \to ({finSupp}_{Z} (R) \leftrightarrow (Fun R \land R supp Z \in Fin))$

Step	Hyp	Ref	Expression
1		funeq	$⊢ r = R \to (Fun r \leftrightarrow Fun R)$
2	1	adantr	$⊢ (r = R \land z = Z) \to (Fun r \leftrightarrow Fun R)$
3		oveq12	$⊢ (r = R \land z = Z) \to r supp z = R supp Z$
4	3	eleq1d	$⊢ (r = R \land z = Z) \to (r supp z \in Fin \leftrightarrow R supp Z \in Fin)$
5	2 4	anbi12d	$⊢ (r = R \land z = Z) \to ((Fun r \land r supp z \in Fin) \leftrightarrow (Fun R \land R supp Z \in Fin))$
6		df-fsupp	$⊢ finSupp = \{⟨r, z⟩ \| (Fun r \land r supp z \in Fin)\}$
7	5 6	brabga	$⊢ (R \in V \land Z \in W) \to ({finSupp}_{Z} (R) \leftrightarrow (Fun R \land R supp Z \in Fin))$

Metamath Proof Explorer