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	|- ( ph -> G e. V )
	fsuppsssuppgd.z	|- ( ph -> Z e. W )
	fsuppsssuppgd.1	|- ( ph -> Fun G )
	fsuppsssuppgd.2	|- ( ph -> F finSupp O )
	fsuppsssuppgd.3	|- ( ph -> ( G supp Z ) C_ ( F supp O ) )
Assertion	fsuppsssuppgd	|- ( ph -> G finSupp Z )

Proof

Step	Hyp	Ref	Expression
1		fsuppsssuppgd.g	|- ( ph -> G e. V )
2		fsuppsssuppgd.z	|- ( ph -> Z e. W )
3		fsuppsssuppgd.1	|- ( ph -> Fun G )
4		fsuppsssuppgd.2	|- ( ph -> F finSupp O )
5		fsuppsssuppgd.3	|- ( ph -> ( G supp Z ) C_ ( F supp O ) )
6	4	fsuppimpd	|- ( ph -> ( F supp O ) e. Fin )
7		suppssfifsupp	|- ( ( ( G e. V /\ Fun G /\ Z e. W ) /\ ( ( F supp O ) e. Fin /\ ( G supp Z ) C_ ( F supp O ) ) ) -> G finSupp Z )
8	1 3 2 6 5 7	syl32anc	|- ( ph -> G finSupp Z )