funisfsupp

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

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

Step	Hyp	Ref	Expression
1		isfsupp	$⊢ (R \in V \land Z \in W) \to ({finSupp}_{Z} (R) \leftrightarrow (Fun R \land R supp Z \in Fin))$
2	1	3adant1	$⊢ (Fun R \land R \in V \land Z \in W) \to ({finSupp}_{Z} (R) \leftrightarrow (Fun R \land R supp Z \in Fin))$
3		ibar	$⊢ Fun R \to (R supp Z \in Fin \leftrightarrow (Fun R \land R supp Z \in Fin))$
4	3	bicomd	$⊢ Fun R \to ((Fun R \land R supp Z \in Fin) \leftrightarrow R supp Z \in Fin)$
5	4	3ad2ant1	$⊢ (Fun R \land R \in V \land Z \in W) \to ((Fun R \land R supp Z \in Fin) \leftrightarrow R supp Z \in Fin)$
6	2 5	bitrd	$⊢ (Fun R \land R \in V \land Z \in W) \to ({finSupp}_{Z} (R) \leftrightarrow R supp Z \in Fin)$

Metamath Proof Explorer