Metamath Proof Explorer

Theorem iiconn

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

Ref Expression
Assertion iiconn 
|- II e. Conn

Proof

Step Hyp Ref Expression
1 dfii2 
 |-  II = ( ( topGen ` ran (,) ) |`t ( 0 [,] 1 ) )
2 0re 
 |-  0 e. RR
3 1re 
 |-  1 e. RR
4 iccconn 
 |-  ( ( 0 e. RR /\ 1 e. RR ) -> ( ( topGen ` ran (,) ) |`t ( 0 [,] 1 ) ) e. Conn )
5 2 3 4 mp2an 
 |-  ( ( topGen ` ran (,) ) |`t ( 0 [,] 1 ) ) e. Conn
6 1 5 eqeltri 
 |-  II e. Conn