Metamath Proof Explorer

Theorem iillysconn

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

Ref Expression
Assertion iillysconn 
|- II e. Locally 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 iccllysconn 
 |-  ( ( 0 e. RR /\ 1 e. RR ) -> ( ( topGen ` ran (,) ) |`t ( 0 [,] 1 ) ) e. Locally SConn )
5 2 3 4 mp2an 
 |-  ( ( topGen ` ran (,) ) |`t ( 0 [,] 1 ) ) e. Locally SConn
6 1 5 eqeltri 
 |-  II e. Locally SConn