suppssfifsupp

Description: If the support of a function is a subset of a finite set, the function is finitely supported. (Contributed by AV, 15-Jul-2019)

		Ref	Expression
	Assertion	suppssfifsupp	$⊢ ((G \in V \land Fun G \land Z \in W) \land (F \in Fin \land G supp Z \subseteq F)) \to {finSupp}_{Z} (G)$

Step	Hyp	Ref	Expression
1		ssfi	$⊢ (F \in Fin \land G supp Z \subseteq F) \to G supp Z \in Fin$
2	1	adantl	$⊢ ((G \in V \land Fun G \land Z \in W) \land (F \in Fin \land G supp Z \subseteq F)) \to G supp Z \in Fin$
3		3ancoma	$⊢ (G \in V \land Fun G \land Z \in W) \leftrightarrow (Fun G \land G \in V \land Z \in W)$
4	3	biimpi	$⊢ (G \in V \land Fun G \land Z \in W) \to (Fun G \land G \in V \land Z \in W)$
5	4	adantr	$⊢ ((G \in V \land Fun G \land Z \in W) \land (F \in Fin \land G supp Z \subseteq F)) \to (Fun G \land G \in V \land Z \in W)$
6		funisfsupp	$⊢ (Fun G \land G \in V \land Z \in W) \to ({finSupp}_{Z} (G) \leftrightarrow G supp Z \in Fin)$
7	5 6	syl	$⊢ ((G \in V \land Fun G \land Z \in W) \land (F \in Fin \land G supp Z \subseteq F)) \to ({finSupp}_{Z} (G) \leftrightarrow G supp Z \in Fin)$
8	2 7	mpbird	$⊢ ((G \in V \land Fun G \land Z \in W) \land (F \in Fin \land G supp Z \subseteq F)) \to {finSupp}_{Z} (G)$

Metamath Proof Explorer