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=BaseK
tsettps.j J=TopSetK
Assertion topontopn JTopOnAJ=TopOpenK

Proof

Step Hyp Ref Expression
1 tsettps.a A=BaseK
2 tsettps.j J=TopSetK
3 toponuni JTopOnAA=J
4 eqimss2 A=JJA
5 3 4 syl JTopOnAJA
6 sspwuni J𝒫AJA
7 5 6 sylibr JTopOnAJ𝒫A
8 1 2 topnid J𝒫AJ=TopOpenK
9 7 8 syl JTopOnAJ=TopOpenK