Description: The composition of a function which maps the zero to zero with a finitely supported function is finitely supported. This is not only a special case of fsuppcor because it does not require that the "zero" is an element of the range of the finitely supported function. (Contributed by AV, 6-Jun-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | fsuppco2.z | |
|
fsuppco2.f | |
||
fsuppco2.g | |
||
fsuppco2.a | |
||
fsuppco2.b | |
||
fsuppco2.n | |
||
fsuppco2.i | |
||
Assertion | fsuppco2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fsuppco2.z | |
|
2 | fsuppco2.f | |
|
3 | fsuppco2.g | |
|
4 | fsuppco2.a | |
|
5 | fsuppco2.b | |
|
6 | fsuppco2.n | |
|
7 | fsuppco2.i | |
|
8 | 3 | ffund | |
9 | 2 | ffund | |
10 | funco | |
|
11 | 8 9 10 | syl2anc | |
12 | 6 | fsuppimpd | |
13 | fco | |
|
14 | 3 2 13 | syl2anc | |
15 | eldifi | |
|
16 | fvco3 | |
|
17 | 2 15 16 | syl2an | |
18 | ssidd | |
|
19 | 2 18 4 1 | suppssr | |
20 | 19 | fveq2d | |
21 | 7 | adantr | |
22 | 17 20 21 | 3eqtrd | |
23 | 14 22 | suppss | |
24 | 12 23 | ssfid | |
25 | 3 5 | fexd | |
26 | 2 4 | fexd | |
27 | coexg | |
|
28 | 25 26 27 | syl2anc | |
29 | isfsupp | |
|
30 | 28 1 29 | syl2anc | |
31 | 11 24 30 | mpbir2and | |