Metamath Proof Explorer


Theorem tpstop

Description: The topology extractor on a topological space is a topology. (Contributed by FL, 27-Jun-2014)

Ref Expression
Hypothesis tpstop.j J=TopOpenK
Assertion tpstop KTopSpJTop

Proof

Step Hyp Ref Expression
1 tpstop.j J=TopOpenK
2 eqid BaseK=BaseK
3 2 1 istps2 KTopSpJTopBaseK=J
4 3 simplbi KTopSpJTop