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 ⁡ ≤ ∈ Conn

Proof

Step Hyp Ref Expression
1 xrhmph ⊢ II ≃ ordTop ⁡ ≤
2 iiconn ⊢ II ∈ Conn
3 connhmph ⊢ II ≃ ordTop ⁡ ≤ → II ∈ Conn → ordTop ⁡ ≤ ∈ Conn
4 1 2 3 mp2 ⊢ ordTop ⁡ ≤ ∈ Conn