Metamath Proof Explorer


Theorem fsuppco2

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 φZW
fsuppco2.f φF:AB
fsuppco2.g φG:BB
fsuppco2.a φAU
fsuppco2.b φBV
fsuppco2.n φfinSuppZF
fsuppco2.i φGZ=Z
Assertion fsuppco2 φfinSuppZGF

Proof

Step Hyp Ref Expression
1 fsuppco2.z φZW
2 fsuppco2.f φF:AB
3 fsuppco2.g φG:BB
4 fsuppco2.a φAU
5 fsuppco2.b φBV
6 fsuppco2.n φfinSuppZF
7 fsuppco2.i φGZ=Z
8 3 ffund φFunG
9 2 ffund φFunF
10 funco FunGFunFFunGF
11 8 9 10 syl2anc φFunGF
12 6 fsuppimpd φFsuppZFin
13 fco G:BBF:ABGF:AB
14 3 2 13 syl2anc φGF:AB
15 eldifi xAsuppZFxA
16 fvco3 F:ABxAGFx=GFx
17 2 15 16 syl2an φxAsuppZFGFx=GFx
18 ssidd φFsuppZFsuppZ
19 2 18 4 1 suppssr φxAsuppZFFx=Z
20 19 fveq2d φxAsuppZFGFx=GZ
21 7 adantr φxAsuppZFGZ=Z
22 17 20 21 3eqtrd φxAsuppZFGFx=Z
23 14 22 suppss φGFsuppZFsuppZ
24 12 23 ssfid φGFsuppZFin
25 3 5 fexd φGV
26 2 4 fexd φFV
27 coexg GVFVGFV
28 25 26 27 syl2anc φGFV
29 isfsupp GFVZWfinSuppZGFFunGFGFsuppZFin
30 28 1 29 syl2anc φfinSuppZGFFunGFGFsuppZFin
31 11 24 30 mpbir2and φfinSuppZGF