Metamath Proof Explorer

Theorem conntop

Description: A connected topology is a topology. (Contributed by FL, 22-Dec-2008) (Revised by Mario Carneiro, 14-Dec-2013)

Ref Expression
Assertion conntop 
|- ( J e. Conn -> J e. Top )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  U. J = U. J
2 1 isconn 
 |-  ( J e. Conn <-> ( J e. Top /\ ( J i^i ( Clsd ` J ) ) = { (/) , U. J } ) )
3 2 simplbi 
 |-  ( J e. Conn -> J e. Top )