Metamath Proof Explorer


Theorem eltpsgOLD

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 K=BasendxATopSetndxJ
Assertion eltpsgOLD JTopOnAKTopSp

Proof

Step Hyp Ref Expression
1 eltpsi.k K=BasendxATopSetndxJ
2 df-tset TopSet=Slot9
3 1lt9 1<9
4 9nn 9
5 1 2 3 4 2strop JTopOnAJ=TopSetK
6 toponmax JTopOnAAJ
7 1 2 3 4 2strbas AJA=BaseK
8 6 7 syl JTopOnAA=BaseK
9 8 fveq2d JTopOnATopOnA=TopOnBaseK
10 5 9 eleq12d JTopOnAJTopOnATopSetKTopOnBaseK
11 10 ibi JTopOnATopSetKTopOnBaseK
12 eqid BaseK=BaseK
13 eqid TopSetK=TopSetK
14 12 13 tsettps TopSetKTopOnBaseKKTopSp
15 11 14 syl JTopOnAKTopSp