Description: If the topology component is already correctly truncated, then it forms a topological space (with the topology extractor function coming out the same as the component). (Contributed by Mario Carneiro, 13-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | tsettps.a | |
|
tsettps.j | |
||
Assertion | tsettps | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tsettps.a | |
|
2 | tsettps.j | |
|
3 | 1 2 | topontopn | |
4 | id | |
|
5 | 3 4 | eqeltrrd | |
6 | eqid | |
|
7 | 1 6 | istps | |
8 | 5 7 | sylibr | |