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