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	⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
	fsuppsssuppgd.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑊 )
	fsuppsssuppgd.1	⊢ ( 𝜑 → Fun 𝐺 )
	fsuppsssuppgd.2	⊢ ( 𝜑 → 𝐹 finSupp 𝑂 )
	fsuppsssuppgd.3	⊢ ( 𝜑 → ( 𝐺 supp 𝑍 ) ⊆ ( 𝐹 supp 𝑂 ) )
Assertion	fsuppsssuppgd	⊢ ( 𝜑 → 𝐺 finSupp 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		fsuppsssuppgd.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
2		fsuppsssuppgd.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑊 )
3		fsuppsssuppgd.1	⊢ ( 𝜑 → Fun 𝐺 )
4		fsuppsssuppgd.2	⊢ ( 𝜑 → 𝐹 finSupp 𝑂 )
5		fsuppsssuppgd.3	⊢ ( 𝜑 → ( 𝐺 supp 𝑍 ) ⊆ ( 𝐹 supp 𝑂 ) )
6	4	fsuppimpd	⊢ ( 𝜑 → ( 𝐹 supp 𝑂 ) ∈ Fin )
7		suppssfifsupp	⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ Fun 𝐺 ∧ 𝑍 ∈ 𝑊 ) ∧ ( ( 𝐹 supp 𝑂 ) ∈ Fin ∧ ( 𝐺 supp 𝑍 ) ⊆ ( 𝐹 supp 𝑂 ) ) ) → 𝐺 finSupp 𝑍 )
8	1 3 2 6 5 7	syl32anc	⊢ ( 𝜑 → 𝐺 finSupp 𝑍 )