Theorem eltpsi

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

	Ref	Expression
Hypotheses	eltpsi.k	|- K = { <. ( Base ` ndx ) , A >. , <. ( TopSet ` ndx ) , J >. }
	eltpsi.u	|- A = U. J
	eltpsi.j	|- J e. Top
Assertion	eltpsi	|- K e. TopSp

Proof

Step	Hyp	Ref	Expression
1		eltpsi.k	|- K = { <. ( Base ` ndx ) , A >. , <. ( TopSet ` ndx ) , J >. }
2		eltpsi.u	|- A = U. J
3		eltpsi.j	|- J e. Top
4	2	toptopon	|- ( J e. Top <-> J e. ( TopOn ` A ) )
5	3 4	mpbi	|- J e. ( TopOn ` A )
6	1	eltpsg	|- ( J e. ( TopOn ` A ) -> K e. TopSp )
7	5 6	ax-mp	|- K e. TopSp