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	|- ( ph -> F C_ G )
	fsuppss.2	|- ( ph -> G finSupp Z )
Assertion	fsuppss	|- ( ph -> F finSupp Z )

Proof

Step	Hyp	Ref	Expression
1		fsuppss.1	|- ( ph -> F C_ G )
2		fsuppss.2	|- ( ph -> G finSupp Z )
3		relfsupp	|- Rel finSupp
4		brrelex1	|- ( ( Rel finSupp /\ G finSupp Z ) -> G e. _V )
5	3 2 4	sylancr	|- ( ph -> G e. _V )
6	5 1	ssexd	|- ( ph -> F e. _V )
7		brrelex2	|- ( ( Rel finSupp /\ G finSupp Z ) -> Z e. _V )
8	3 2 7	sylancr	|- ( ph -> Z e. _V )
9	2	fsuppfund	|- ( ph -> Fun G )
10		funss	|- ( F C_ G -> ( Fun G -> Fun F ) )
11	1 9 10	sylc	|- ( ph -> Fun F )
12		funsssuppss	|- ( ( Fun G /\ F C_ G /\ G e. _V ) -> ( F supp Z ) C_ ( G supp Z ) )
13	9 1 5 12	syl3anc	|- ( ph -> ( F supp Z ) C_ ( G supp Z ) )
14	6 8 11 2 13	fsuppsssuppgd	|- ( ph -> F finSupp Z )