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
|- ( 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 )