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

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 )