Metamath Proof Explorer

Theorem fsuppsssupp

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

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

Proof

Step	Hyp	Ref	Expression
1		simpll	$⊢ ((G \in V \land Fun G) \land ({finSupp}_{Z} (F) \land G supp Z \subseteq F supp Z)) \to G \in V$
2		simplr	$⊢ ((G \in V \land Fun G) \land ({finSupp}_{Z} (F) \land G supp Z \subseteq F supp Z)) \to Fun G$
3		relfsupp	$⊢ Rel finSupp$
4	3	brrelex2i	$⊢ {finSupp}_{Z} (F) \to Z \in V$
5	4	ad2antrl	$⊢ ((G \in V \land Fun G) \land ({finSupp}_{Z} (F) \land G supp Z \subseteq F supp Z)) \to Z \in V$
6		id	$⊢ {finSupp}_{Z} (F) \to {finSupp}_{Z} (F)$
7	6	fsuppimpd	$⊢ {finSupp}_{Z} (F) \to F supp Z \in Fin$
8	7	anim1i	$⊢ ({finSupp}_{Z} (F) \land G supp Z \subseteq F supp Z) \to (F supp Z \in Fin \land G supp Z \subseteq F supp Z)$
9	8	adantl	$⊢ ((G \in V \land Fun G) \land ({finSupp}_{Z} (F) \land G supp Z \subseteq F supp Z)) \to (F supp Z \in Fin \land G supp Z \subseteq F supp Z)$
10		suppssfifsupp	$⊢ ((G \in V \land Fun G \land Z \in V) \land (F supp Z \in Fin \land G supp Z \subseteq F supp Z)) \to {finSupp}_{Z} (G)$
11	1 2 5 9 10	syl31anc	$⊢ ((G \in V \land Fun G) \land ({finSupp}_{Z} (F) \land G supp Z \subseteq F supp Z)) \to {finSupp}_{Z} (G)$