Metamath Proof Explorer

Theorem xrconn

Description: The topology of the extended reals is connected. (Contributed by Mario Carneiro, 9-Sep-2015)

Ref Expression
Assertion xrconn 
|- ( ordTop ` <_ ) e. Conn

Proof

Step Hyp Ref Expression
1 xrhmph 
 |-  II ~= ( ordTop ` <_ )
2 iiconn 
 |-  II e. Conn
3 connhmph 
 |-  ( II ~= ( ordTop ` <_ ) -> ( II e. Conn -> ( ordTop ` <_ ) e. Conn ) )
4 1 2 3 mp2 
 |-  ( ordTop ` <_ ) e. Conn