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