Theorem topontopn

Description: Express the predicate "is a topological space." (Contributed by Mario Carneiro, 13-Aug-2015)

	Ref	Expression
Hypotheses	tsettps.a	$$⊢A={\mathrm{Base}}_K$$
	tsettps.j	$$⊢J=\mathrm{TopSet}\left(K\right)$$
Assertion	topontopn	$$⊢J\in \mathrm{TopOn}\left(A\right)\to J=\mathrm{TopOpen}\left(K\right)$$

Proof

Step	Hyp	Ref	Expression
1		tsettps.a	$$⊢A={\mathrm{Base}}_K$$
2		tsettps.j	$$⊢J=\mathrm{TopSet}\left(K\right)$$
3		toponuni	$$⊢J\in \mathrm{TopOn}\left(A\right)\to A=\bigcup J$$
4		eqimss2	$$⊢A=\bigcup J\to \bigcup J\subseteq A$$
5	3 4	syl	$$⊢J\in \mathrm{TopOn}\left(A\right)\to \bigcup J\subseteq A$$
6		sspwuni	$$⊢J\subseteq 𝒫A\leftrightarrow \bigcup J\subseteq A$$
7	5 6	sylibr	$$⊢J\in \mathrm{TopOn}\left(A\right)\to J\subseteq 𝒫A$$
8	1 2	topnid	$$⊢J\subseteq 𝒫A\to J=\mathrm{TopOpen}\left(K\right)$$
9	7 8	syl	$$⊢J\in \mathrm{TopOn}\left(A\right)\to J=\mathrm{TopOpen}\left(K\right)$$