fsuppss

Description: A subset of a finitely supported function is a finitely supported function. (Contributed by SN, 8-Mar-2025)

Step	Hyp	Ref	Expression
1		fsuppss.1	$⊢ φ \to F \subseteq G$
2		fsuppss.2	$⊢ φ \to {finSupp}_{Z} (G)$
3		relfsupp	$⊢ Rel finSupp$
4		brrelex1	$⊢ (Rel finSupp \land {finSupp}_{Z} (G)) \to G \in V$
5	3 2 4	sylancr	$⊢ φ \to G \in V$
6	5 1	ssexd	$⊢ φ \to F \in V$
7		brrelex2	$⊢ (Rel finSupp \land {finSupp}_{Z} (G)) \to Z \in V$
8	3 2 7	sylancr	$⊢ φ \to Z \in V$
9	2	fsuppfund	$⊢ φ \to Fun G$
10		funss	$⊢ F \subseteq G \to (Fun G \to Fun F)$
11	1 9 10	sylc	$⊢ φ \to Fun F$
12		funsssuppss	$⊢ (Fun G \land F \subseteq G \land G \in V) \to F supp Z \subseteq G supp Z$
13	9 1 5 12	syl3anc	$⊢ φ \to F supp Z \subseteq G supp Z$
14	6 8 11 2 13	fsuppsssuppgd	$⊢ φ \to {finSupp}_{Z} (F)$

Metamath Proof Explorer