This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = Base K
tsettps.j ⊢ J = TopSet ⁡ K
Assertion topontopn ⊢ J ∈ TopOn ⁡ A → J = TopOpen ⁡ K

Proof

Step Hyp Ref Expression
1 tsettps.a ⊢ A = Base K
2 tsettps.j ⊢ J = TopSet ⁡ K
3 toponuni ⊢ J ∈ TopOn ⁡ A → A = ⋃ J
4 eqimss2 ⊢ A = ⋃ J → ⋃ J ⊆ A
5 3 4 syl ⊢ J ∈ TopOn ⁡ A → ⋃ J ⊆ A
6 sspwuni ⊢ J ⊆ 𝒫 A ↔ ⋃ J ⊆ A
7 5 6 sylibr ⊢ J ∈ TopOn ⁡ A → J ⊆ 𝒫 A
8 1 2 topnid ⊢ J ⊆ 𝒫 A → J = TopOpen ⁡ K
9 7 8 syl ⊢ J ∈ TopOn ⁡ A → J = TopOpen ⁡ K