Theorem fmptssfisupp

Description: The restriction of a mapping function has finite support if that function has finite support. (Contributed by Thierry Arnoux, 21-Jan-2024)

	Ref	Expression
Hypotheses	fmptssfisupp.1	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) finSupp 𝑍 )
	fmptssfisupp.2	⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
	fmptssfisupp.3	⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
Assertion	fmptssfisupp	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↦ 𝐵 ) finSupp 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		fmptssfisupp.1	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) finSupp 𝑍 )
2		fmptssfisupp.2	⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
3		fmptssfisupp.3	⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
4	2	resmptd	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝐶 ) = ( 𝑥 ∈ 𝐶 ↦ 𝐵 ) )
5	1 3	fsuppres	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝐶 ) finSupp 𝑍 )
6	4 5	eqbrtrrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↦ 𝐵 ) finSupp 𝑍 )