Theorem fsuppss

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

	Ref	Expression
Hypotheses	fsuppss.1	$$⊢\phi \to F\subseteq G$$
	fsuppss.2	$$⊢\phi \to {finSupp}_Z\left(G\right)$$
Assertion	fsuppss	$$⊢\phi \to {finSupp}_Z\left(F\right)$$

Proof

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