Description: One half of tgptsmscls , true in any commutative monoid topological space. (Contributed by Mario Carneiro, 21-Sep-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | tsmscls.b | |
|
tsmscls.j | |
||
tsmscls.1 | |
||
tsmscls.2 | |
||
tsmscls.a | |
||
tsmscls.f | |
||
tsmscls.x | |
||
Assertion | tsmscls | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tsmscls.b | |
|
2 | tsmscls.j | |
|
3 | tsmscls.1 | |
|
4 | tsmscls.2 | |
|
5 | tsmscls.a | |
|
6 | tsmscls.f | |
|
7 | tsmscls.x | |
|
8 | eqid | |
|
9 | eqid | |
|
10 | 1 2 8 9 4 5 6 | tsmsval | |
11 | 1 2 | istps | |
12 | 4 11 | sylib | |
13 | eqid | |
|
14 | 8 13 9 5 | tsmsfbas | |
15 | fgcl | |
|
16 | 14 15 | syl | |
17 | 1 8 3 5 6 | tsmslem1 | |
18 | 17 | fmpttd | |
19 | flfval | |
|
20 | 12 16 18 19 | syl3anc | |
21 | 10 20 | eqtrd | |
22 | 7 21 | eleqtrd | |
23 | flimsncls | |
|
24 | 22 23 | syl | |
25 | 24 21 | sseqtrrd | |