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 ) |
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 ) |