Metamath Proof Explorer


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 Z x A B
fmptssfisupp.2 φ C A
fmptssfisupp.3 φ Z V
Assertion fmptssfisupp φ finSupp Z x C B

Proof

Step Hyp Ref Expression
1 fmptssfisupp.1 φ finSupp Z x A B
2 fmptssfisupp.2 φ C A
3 fmptssfisupp.3 φ Z V
4 2 resmptd φ x A B C = x C B
5 1 3 fsuppres φ finSupp Z x A B C
6 4 5 eqbrtrrd φ finSupp Z x C B