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 Conn J Top

Proof

Step Hyp Ref Expression
1 eqid J = J
2 1 isconn J Conn J Top J Clsd J = J
3 2 simplbi J Conn J Top