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)

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 df-tset
 |-  TopSet = Slot 9
3 1lt9
 |-  1 < 9
4 9nn
 |-  9 e. NN
5 1 2 3 4 2strop
 |-  ( J e. ( TopOn ` A ) -> J = ( TopSet ` K ) )
6 toponmax
 |-  ( J e. ( TopOn ` A ) -> A e. J )
7 1 2 3 4 2strbas
 |-  ( 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 )