# Metamath Proof Explorer

## 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}↔\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)$