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 )