This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ φ \to G \in V$
		fsuppsssuppgd.z	$⊢ φ \to Z \in W$
		fsuppsssuppgd.1	$⊢ φ \to Fun G$
		fsuppsssuppgd.2	$⊢ φ \to {finSupp}_{O} (F)$
		fsuppsssuppgd.3	$⊢ φ \to G supp Z \subseteq F supp O$
	Assertion	fsuppsssuppgd	$⊢ φ \to {finSupp}_{Z} (G)$

Proof

Step	Hyp	Ref	Expression
1		fsuppsssuppgd.g	$⊢ φ \to G \in V$
2		fsuppsssuppgd.z	$⊢ φ \to Z \in W$
3		fsuppsssuppgd.1	$⊢ φ \to Fun G$
4		fsuppsssuppgd.2	$⊢ φ \to {finSupp}_{O} (F)$
5		fsuppsssuppgd.3	$⊢ φ \to G supp Z \subseteq F supp O$
6	4	fsuppimpd	$⊢ φ \to F supp O \in Fin$
7		suppssfifsupp	$⊢ ((G \in V \land Fun G \land Z \in W) \land (F supp O \in Fin \land G supp Z \subseteq F supp O)) \to {finSupp}_{Z} (G)$
8	1 3 2 6 5 7	syl32anc	$⊢ φ \to {finSupp}_{Z} (G)$