Theorem iinllyconn

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

	Ref	Expression
Assertion	iinllyconn	|- II e. N-Locally Conn

Proof

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