Theorem istpsi

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

	Ref	Expression
Hypotheses	istpsi.b	$$⊢{\mathrm{Base}}_K=A$$
	istpsi.j	$$⊢\mathrm{TopOpen}\left(K\right)=J$$
	istpsi.1	$$⊢A=\bigcup J$$
	istpsi.2	$$⊢J\in \mathrm{Top}$$
Assertion	istpsi	$$⊢K\in \mathrm{TopSp}$$

Proof

Step	Hyp	Ref	Expression
1		istpsi.b	$$⊢{\mathrm{Base}}_K=A$$
2		istpsi.j	$$⊢\mathrm{TopOpen}\left(K\right)=J$$
3		istpsi.1	$$⊢A=\bigcup J$$
4		istpsi.2	$$⊢J\in \mathrm{Top}$$
5	1	eqcomi	$$⊢A={\mathrm{Base}}_K$$
6	2	eqcomi	$$⊢J=\mathrm{TopOpen}\left(K\right)$$
7	5 6	istps2	$$⊢K\in \mathrm{TopSp}\leftrightarrow \left(J\in \mathrm{Top}\wedge A=\bigcup J\right)$$
8	4 3 7	mpbir2an	$$⊢K\in \mathrm{TopSp}$$