Theorem istpsi

Description: Properties that determine a topological space. (Contributed by NM, 20-Oct-2012)

	Ref	Expression
Hypotheses	istpsi.b	|- ( Base ` K ) = A
	istpsi.j	|- ( TopOpen ` K ) = J
	istpsi.1	|- A = U. J
	istpsi.2	|- J e. Top
Assertion	istpsi	|- K e. TopSp

Proof

Step	Hyp	Ref	Expression
1		istpsi.b	|- ( Base ` K ) = A
2		istpsi.j	|- ( TopOpen ` K ) = J
3		istpsi.1	|- A = U. J
4		istpsi.2	|- J e. Top
5	1	eqcomi	|- A = ( Base ` K )
6	2	eqcomi	|- J = ( TopOpen ` K )
7	5 6	istps2	|- ( K e. TopSp <-> ( J e. Top /\ A = U. J ) )
8	4 3 7	mpbir2an	|- K e. TopSp