Theorem retopconn

Description: Corollary of reconn . The set of real numbers is connected. (Contributed by Jeff Hankins, 17-Aug-2009)

	Ref	Expression
Assertion	retopconn	⊢ ( topGen ‘ ran (,) ) ∈ Conn

Proof

Step	Hyp	Ref	Expression
1		retop	⊢ ( topGen ‘ ran (,) ) ∈ Top
2		uniretop	⊢ ℝ = ∪ ( topGen ‘ ran (,) )
3	2	restid	⊢ ( ( topGen ‘ ran (,) ) ∈ Top → ( ( topGen ‘ ran (,) ) ↾t ℝ ) = ( topGen ‘ ran (,) ) )
4	1 3	ax-mp	⊢ ( ( topGen ‘ ran (,) ) ↾t ℝ ) = ( topGen ‘ ran (,) )
5		iccssre	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 [,] 𝑦 ) ⊆ ℝ )
6	5	rgen2	⊢ ∀ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℝ ( 𝑥 [,] 𝑦 ) ⊆ ℝ
7		ssid	⊢ ℝ ⊆ ℝ
8		reconn	⊢ ( ℝ ⊆ ℝ → ( ( ( topGen ‘ ran (,) ) ↾t ℝ ) ∈ Conn ↔ ∀ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℝ ( 𝑥 [,] 𝑦 ) ⊆ ℝ ) )
9	7 8	ax-mp	⊢ ( ( ( topGen ‘ ran (,) ) ↾t ℝ ) ∈ Conn ↔ ∀ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℝ ( 𝑥 [,] 𝑦 ) ⊆ ℝ )
10	6 9	mpbir	⊢ ( ( topGen ‘ ran (,) ) ↾t ℝ ) ∈ Conn
11	4 10	eqeltrri	⊢ ( topGen ‘ ran (,) ) ∈ Conn