Theorem tpsuni

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

	Ref	Expression
Hypotheses	istps.a	$$⊢A={\mathrm{Base}}_K$$
	istps.j	$$⊢J=\mathrm{TopOpen}\left(K\right)$$
Assertion	tpsuni	$$⊢K\in \mathrm{TopSp}\to A=\bigcup J$$

Proof

Step	Hyp	Ref	Expression
1		istps.a	$$⊢A={\mathrm{Base}}_K$$
2		istps.j	$$⊢J=\mathrm{TopOpen}\left(K\right)$$
3	1 2	istps2	$$⊢K\in \mathrm{TopSp}\leftrightarrow \left(J\in \mathrm{Top}\wedge A=\bigcup J\right)$$
4	3	simprbi	$$⊢K\in \mathrm{TopSp}\to A=\bigcup J$$