Theorem fsuppsssuppgd

Description: If the support of a function is a subset of a finite support, it is finite. Deduction associated with fsuppsssupp . (Contributed by SN, 6-Mar-2025)

	Ref	Expression
Hypotheses	fsuppsssuppgd.g	$$⊢\phi \to G\in V$$
	fsuppsssuppgd.z	$$⊢\phi \to Z\in W$$
	fsuppsssuppgd.1	$$⊢\phi \to \mathrm{Fun}G$$
	fsuppsssuppgd.2	$$⊢\phi \to {finSupp}_O\left(F\right)$$
	fsuppsssuppgd.3	$$⊢\phi \to G\mathrm{supp}Z\subseteq F\mathrm{supp}O$$
Assertion	fsuppsssuppgd	$$⊢\phi \to {finSupp}_Z\left(G\right)$$

Proof

Step	Hyp	Ref	Expression
1		fsuppsssuppgd.g	$$⊢\phi \to G\in V$$
2		fsuppsssuppgd.z	$$⊢\phi \to Z\in W$$
3		fsuppsssuppgd.1	$$⊢\phi \to \mathrm{Fun}G$$
4		fsuppsssuppgd.2	$$⊢\phi \to {finSupp}_O\left(F\right)$$
5		fsuppsssuppgd.3	$$⊢\phi \to G\mathrm{supp}Z\subseteq F\mathrm{supp}O$$
6	4	fsuppimpd	$$⊢\phi \to F\mathrm{supp}O\in \mathrm{Fin}$$
7		suppssfifsupp	$$⊢\left(\left(G\in V\wedge \mathrm{Fun}G\wedge Z\in W\right)\wedge \left(F\mathrm{supp}O\in \mathrm{Fin}\wedge G\mathrm{supp}Z\subseteq F\mathrm{supp}O\right)\right)\to {finSupp}_Z\left(G\right)$$
8	1 3 2 6 5 7	syl32anc	$$⊢\phi \to {finSupp}_Z\left(G\right)$$