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	$$⊢\phi \to {finSupp}_Z\left(\left(x\in A⟼B\right)\right)$$
	fmptssfisupp.2	$$⊢\phi \to C\subseteq A$$
	fmptssfisupp.3	$$⊢\phi \to Z\in V$$
Assertion	fmptssfisupp	$$⊢\phi \to {finSupp}_Z\left(\left(x\in C⟼B\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		fmptssfisupp.1	$$⊢\phi \to {finSupp}_Z\left(\left(x\in A⟼B\right)\right)$$
2		fmptssfisupp.2	$$⊢\phi \to C\subseteq A$$
3		fmptssfisupp.3	$$⊢\phi \to Z\in V$$
4	2	resmptd	$$⊢\phi \to {\left(x\in A⟼B\right)\upharpoonright }_C=\left(x\in C⟼B\right)$$
5	1 3	fsuppres	$$⊢\phi \to {finSupp}_Z\left(\left({\left(x\in A⟼B\right)\upharpoonright }_C\right)\right)$$
6	4 5	eqbrtrrd	$$⊢\phi \to {finSupp}_Z\left(\left(x\in C⟼B\right)\right)$$