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