This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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