Description: Express the predicate "is a topological space." (Contributed by Mario Carneiro, 13-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | tsettps.a | |
|
tsettps.j | |
||
Assertion | topontopn | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tsettps.a | |
|
2 | tsettps.j | |
|
3 | toponuni | |
|
4 | eqimss2 | |
|
5 | 3 4 | syl | |
6 | sspwuni | |
|
7 | 5 6 | sylibr | |
8 | 1 2 | topnid | |
9 | 7 8 | syl | |