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 | ||
fmptssfisupp.2 | |||
fmptssfisupp.3 | |||
Assertion | fmptssfisupp |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fmptssfisupp.1 | ||
2 | fmptssfisupp.2 | ||
3 | fmptssfisupp.3 | ||
4 | 2 | resmptd | |
5 | 1 3 | fsuppres | |
6 | 4 5 | eqbrtrrd |