Description: The unit interval is connected. (Contributed by Mario Carneiro, 11-Feb-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | iiconn | ⊢ II ∈ Conn |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfii2 | ⊢ II = ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] 1 ) ) | |
2 | 0re | ⊢ 0 ∈ ℝ | |
3 | 1re | ⊢ 1 ∈ ℝ | |
4 | iccconn | ⊢ ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] 1 ) ) ∈ Conn ) | |
5 | 2 3 4 | mp2an | ⊢ ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] 1 ) ) ∈ Conn |
6 | 1 5 | eqeltri | ⊢ II ∈ Conn |