Theorem tpsuni

Description: The base set of a topological space. (Contributed by FL, 27-Jun-2014)

	Ref	Expression
Hypotheses	istps.a	|- A = ( Base ` K )
	istps.j	|- J = ( TopOpen ` K )
Assertion	tpsuni	|- ( K e. TopSp -> A = U. J )

Proof

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