iinllyconn

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

		Ref	Expression
	Assertion	iinllyconn	$⊢ II \in N-LocallyConn$

Step	Hyp	Ref	Expression
1		sconnpconn	$⊢ x \in SConn \to x \in PConn$
2		pconnconn	$⊢ x \in PConn \to x \in Conn$
3	1 2	syl	$⊢ x \in SConn \to x \in Conn$
4	3	ssriv	$⊢ SConn \subseteq Conn$
5		nllyss	$⊢ SConn \subseteq Conn \to N-LocallySConn\subseteqN-LocallyConn$
6	4 5	ax-mp	$⊢ N-LocallySConn\subseteqN-LocallyConn$
7		llyssnlly	$⊢ LocallySConn\subseteqN-LocallySConn$
8		iillysconn	$⊢ II \in LocallySConn$
9	7 8	sselii	$⊢ II \in N-LocallySConn$
10	6 9	sselii	$⊢ II \in N-LocallyConn$

Metamath Proof Explorer