Metamath Proof Explorer

Theorem fsuppimp

Description: Implications of a class being a finitely supported function (in relation to a given zero). (Contributed by AV, 26-May-2019)

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

Step	Hyp	Ref	Expression
1		relfsupp	$⊢ Rel finSupp$
2	1	brrelex12i	$⊢ {finSupp}_{Z} (R) \to (R \in V \land Z \in V)$
3		isfsupp	$⊢ (R \in V \land Z \in V) \to ({finSupp}_{Z} (R) \leftrightarrow (Fun R \land R supp Z \in Fin))$
4	3	biimpd	$⊢ (R \in V \land Z \in V) \to ({finSupp}_{Z} (R) \to (Fun R \land R supp Z \in Fin))$
5	2 4	mpcom	$⊢ {finSupp}_{Z} (R) \to (Fun R \land R supp Z \in Fin)$