Theorem istps2

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

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

Proof

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