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	⊢ ( 𝜑 → 𝐹 ⊆ 𝐺 )
	fsuppss.2	⊢ ( 𝜑 → 𝐺 finSupp 𝑍 )
Assertion	fsuppss	⊢ ( 𝜑 → 𝐹 finSupp 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		fsuppss.1	⊢ ( 𝜑 → 𝐹 ⊆ 𝐺 )
2		fsuppss.2	⊢ ( 𝜑 → 𝐺 finSupp 𝑍 )
3		relfsupp	⊢ Rel finSupp
4		brrelex1	⊢ ( ( Rel finSupp ∧ 𝐺 finSupp 𝑍 ) → 𝐺 ∈ V )
5	3 2 4	sylancr	⊢ ( 𝜑 → 𝐺 ∈ V )
6	5 1	ssexd	⊢ ( 𝜑 → 𝐹 ∈ V )
7		brrelex2	⊢ ( ( Rel finSupp ∧ 𝐺 finSupp 𝑍 ) → 𝑍 ∈ V )
8	3 2 7	sylancr	⊢ ( 𝜑 → 𝑍 ∈ V )
9	2	fsuppfund	⊢ ( 𝜑 → Fun 𝐺 )
10		funss	⊢ ( 𝐹 ⊆ 𝐺 → ( Fun 𝐺 → Fun 𝐹 ) )
11	1 9 10	sylc	⊢ ( 𝜑 → Fun 𝐹 )
12		funsssuppss	⊢ ( ( Fun 𝐺 ∧ 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ V ) → ( 𝐹 supp 𝑍 ) ⊆ ( 𝐺 supp 𝑍 ) )
13	9 1 5 12	syl3anc	⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) ⊆ ( 𝐺 supp 𝑍 ) )
14	6 8 11 2 13	fsuppsssuppgd	⊢ ( 𝜑 → 𝐹 finSupp 𝑍 )