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 )