Metamath Proof Explorer


Theorem eltpsg

Description: Properties that determine a topological space from a construction (using no explicit indices). (Contributed by Mario Carneiro, 13-Aug-2015) (Revised by AV, 31-Oct-2024)

Ref Expression
Hypothesis eltpsi.k
|- K = { <. ( Base ` ndx ) , A >. , <. ( TopSet ` ndx ) , J >. }
Assertion eltpsg
|- ( J e. ( TopOn ` A ) -> K e. TopSp )

Proof

Step Hyp Ref Expression
1 eltpsi.k
 |-  K = { <. ( Base ` ndx ) , A >. , <. ( TopSet ` ndx ) , J >. }
2 basendxlttsetndx
 |-  ( Base ` ndx ) < ( TopSet ` ndx )
3 tsetndxnn
 |-  ( TopSet ` ndx ) e. NN
4 tsetid
 |-  TopSet = Slot ( TopSet ` ndx )
5 1 2 3 4 2strop1
 |-  ( J e. ( TopOn ` A ) -> J = ( TopSet ` K ) )
6 toponmax
 |-  ( J e. ( TopOn ` A ) -> A e. J )
7 1 2 3 2strbas1
 |-  ( A e. J -> A = ( Base ` K ) )
8 6 7 syl
 |-  ( J e. ( TopOn ` A ) -> A = ( Base ` K ) )
9 8 fveq2d
 |-  ( J e. ( TopOn ` A ) -> ( TopOn ` A ) = ( TopOn ` ( Base ` K ) ) )
10 5 9 eleq12d
 |-  ( J e. ( TopOn ` A ) -> ( J e. ( TopOn ` A ) <-> ( TopSet ` K ) e. ( TopOn ` ( Base ` K ) ) ) )
11 10 ibi
 |-  ( J e. ( TopOn ` A ) -> ( TopSet ` K ) e. ( TopOn ` ( Base ` K ) ) )
12 eqid
 |-  ( Base ` K ) = ( Base ` K )
13 eqid
 |-  ( TopSet ` K ) = ( TopSet ` K )
14 12 13 tsettps
 |-  ( ( TopSet ` K ) e. ( TopOn ` ( Base ` K ) ) -> K e. TopSp )
15 11 14 syl
 |-  ( J e. ( TopOn ` A ) -> K e. TopSp )