Metamath Proof Explorer

Theorem ordtopconn

Description: An ordinal topology is connected. (Contributed by Chen-Pang He, 1-Nov-2015)

Ref Expression
Assertion ordtopconn 
|- ( Ord J -> ( J e. Top <-> J e. Conn ) )

Proof

Step Hyp Ref Expression
1 ordtop 
 |-  ( Ord J -> ( J e. Top <-> J =/= U. J ) )
2 onsucconn 
 |-  ( U. J e. On -> suc U. J e. Conn )
3 2 ordtoplem 
 |-  ( Ord J -> ( J =/= U. J -> J e. Conn ) )
4 1 3 sylbid 
 |-  ( Ord J -> ( J e. Top -> J e. Conn ) )
5 conntop 
 |-  ( J e. Conn -> J e. Top )
6 4 5 impbid1 
 |-  ( Ord J -> ( J e. Top <-> J e. Conn ) )