Metamath Proof Explorer


Theorem iccconn

Description: A closed interval is connected. (Contributed by Jeff Hankins, 17-Aug-2009)

Ref Expression
Assertion iccconn ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ∈ Conn )

Proof

Step Hyp Ref Expression
1 iccss2 ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑥 [,] 𝑦 ) ⊆ ( 𝐴 [,] 𝐵 ) )
2 1 rgen2 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( 𝑥 [,] 𝑦 ) ⊆ ( 𝐴 [,] 𝐵 )
3 iccssre ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
4 reconn ( ( 𝐴 [,] 𝐵 ) ⊆ ℝ → ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ∈ Conn ↔ ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( 𝑥 [,] 𝑦 ) ⊆ ( 𝐴 [,] 𝐵 ) ) )
5 3 4 syl ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ∈ Conn ↔ ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( 𝑥 [,] 𝑦 ) ⊆ ( 𝐴 [,] 𝐵 ) ) )
6 2 5 mpbiri ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ∈ Conn )