Metamath Proof Explorer

Theorem iisconn

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

Ref Expression
Assertion iisconn 
|- II e. SConn

Proof

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