Theorem retopsconn

Description: The real numbers are simply connected. (Contributed by Mario Carneiro, 9-Mar-2015)

	Ref	Expression
Assertion	retopsconn	⊢ ( topGen ‘ ran (,) ) ∈ SConn

Proof

Step	Hyp	Ref	Expression
1		retop	⊢ ( topGen ‘ ran (,) ) ∈ Top
2		ioomax	⊢ ( -∞ (,) +∞ ) = ℝ
3		uniretop	⊢ ℝ = ∪ ( topGen ‘ ran (,) )
4	2 3	eqtri	⊢ ( -∞ (,) +∞ ) = ∪ ( topGen ‘ ran (,) )
5	4	restid	⊢ ( ( topGen ‘ ran (,) ) ∈ Top → ( ( topGen ‘ ran (,) ) ↾t ( -∞ (,) +∞ ) ) = ( topGen ‘ ran (,) ) )
6	1 5	ax-mp	⊢ ( ( topGen ‘ ran (,) ) ↾t ( -∞ (,) +∞ ) ) = ( topGen ‘ ran (,) )
7		ioosconn	⊢ ( ( topGen ‘ ran (,) ) ↾t ( -∞ (,) +∞ ) ) ∈ SConn
8	6 7	eqeltrri	⊢ ( topGen ‘ ran (,) ) ∈ SConn