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	|- ( ph -> ( x e. A |-> B ) finSupp Z )
	fmptssfisupp.2	|- ( ph -> C C_ A )
	fmptssfisupp.3	|- ( ph -> Z e. V )
Assertion	fmptssfisupp	|- ( ph -> ( x e. C |-> B ) finSupp Z )

Proof

Step	Hyp	Ref	Expression
1		fmptssfisupp.1	|- ( ph -> ( x e. A |-> B ) finSupp Z )
2		fmptssfisupp.2	|- ( ph -> C C_ A )
3		fmptssfisupp.3	|- ( ph -> Z e. V )
4	2	resmptd	|- ( ph -> ( ( x e. A |-> B ) |` C ) = ( x e. C |-> B ) )
5	1 3	fsuppres	|- ( ph -> ( ( x e. A |-> B ) |` C ) finSupp Z )
6	4 5	eqbrtrrd	|- ( ph -> ( x e. C |-> B ) finSupp Z )