Metamath Proof Explorer


Theorem iiconn

Description: The unit interval is connected. (Contributed by Mario Carneiro, 11-Feb-2015)

Ref Expression
Assertion iiconn II ∈ Conn

Proof

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