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 )