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