Description: Obsolete version of eltpsg as of 31-Oct-2024. Properties that determine a topological space from a construction (using no explicit indices). (Contributed by Mario Carneiro, 13-Aug-2015) (New usage is discouraged.) (Proof modification is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypothesis | eltpsi.k | |
|
Assertion | eltpsgOLD | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eltpsi.k | |
|
2 | df-tset | |
|
3 | 1lt9 | |
|
4 | 9nn | |
|
5 | 1 2 3 4 | 2strop | |
6 | toponmax | |
|
7 | 1 2 3 4 | 2strbas | |
8 | 6 7 | syl | |
9 | 8 | fveq2d | |
10 | 5 9 | eleq12d | |
11 | 10 | ibi | |
12 | eqid | |
|
13 | eqid | |
|
14 | 12 13 | tsettps | |
15 | 11 14 | syl | |