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 = ( TopOpen ` K )
Assertion tpstop 
|- ( K e. TopSp -> J e. Top )

Proof

Step Hyp Ref Expression
1 tpstop.j 
 |-  J = ( TopOpen ` K )
2 eqid 
 |-  ( Base ` K ) = ( Base ` K )
3 2 1 istps2 
 |-  ( K e. TopSp <-> ( J e. Top /\ ( Base ` K ) = U. J ) )
4 3 simplbi 
 |-  ( K e. TopSp -> J e. Top )