Metamath Proof Explorer


Theorem iinllyconn

Description: The unit interval is locally connected. (Contributed by Mario Carneiro, 6-Jul-2015)

Ref Expression
Assertion iinllyconn II N-Locally Conn

Proof

Step Hyp Ref Expression
1 sconnpconn x SConn x PConn
2 pconnconn x PConn x Conn
3 1 2 syl x SConn x Conn
4 3 ssriv SConn Conn
5 nllyss SConn Conn N-Locally SConn N-Locally Conn
6 4 5 ax-mp N-Locally SConn N-Locally Conn
7 llyssnlly Locally SConn N-Locally SConn
8 iillysconn II Locally SConn
9 7 8 sselii II N-Locally SConn
10 6 9 sselii II N-Locally Conn