Description: The union of the support of two finitely supported functions is finite. (Contributed by AV, 1-Jul-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | fsuppun.f | |
|
fsuppun.g | |
||
Assertion | fsuppunfi | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fsuppun.f | |
|
2 | fsuppun.g | |
|
3 | fsuppimp | |
|
4 | fsuppimp | |
|
5 | unfi | |
|
6 | 5 | expcom | |
7 | 6 | adantl | |
8 | 2 4 7 | 3syl | |
9 | 8 | com12 | |
10 | 3 9 | simpl2im | |
11 | 1 10 | mpcom | |