Theorem istps2

Description: Express the predicate "is a topological space." (Contributed by NM, 20-Oct-2012)

	Ref	Expression
Hypotheses	istps.a	|- A = ( Base ` K )
	istps.j	|- J = ( TopOpen ` K )
Assertion	istps2	|- ( K e. TopSp <-> ( J e. Top /\ A = U. J ) )

Proof

Step	Hyp	Ref	Expression
1		istps.a	|- A = ( Base ` K )
2		istps.j	|- J = ( TopOpen ` K )
3	1 2	istps	|- ( K e. TopSp <-> J e. ( TopOn ` A ) )
4		istopon	|- ( J e. ( TopOn ` A ) <-> ( J e. Top /\ A = U. J ) )
5	3 4	bitri	|- ( K e. TopSp <-> ( J e. Top /\ A = U. J ) )