Theorem iccsconn

Description: A closed interval is simply connected. (Contributed by Mario Carneiro, 9-Mar-2015)

	Ref	Expression
Assertion	iccsconn	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ∈ SConn )

Proof

Step	Hyp	Ref	Expression
1		iccconn	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ∈ Conn )
2		iccssre	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
3		eqid	⊢ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) = ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) )
4	3	resconn	⊢ ( ( 𝐴 [,] 𝐵 ) ⊆ ℝ → ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ∈ SConn ↔ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ∈ Conn ) )
5	2 4	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ∈ SConn ↔ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ∈ Conn ) )
6	1 5	mpbird	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ∈ SConn )