Theorem iinllyconn

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

	Ref	Expression
Assertion	iinllyconn	⊢ II ∈ 𝑛-Locally Conn

Proof

Step	Hyp	Ref	Expression
1		sconnpconn	⊢ ( 𝑥 ∈ SConn → 𝑥 ∈ PConn )
2		pconnconn	⊢ ( 𝑥 ∈ PConn → 𝑥 ∈ Conn )
3	1 2	syl	⊢ ( 𝑥 ∈ SConn → 𝑥 ∈ Conn )
4	3	ssriv	⊢ SConn ⊆ Conn
5		nllyss	⊢ ( SConn ⊆ Conn → 𝑛-Locally SConn ⊆ 𝑛-Locally Conn )
6	4 5	ax-mp	⊢ 𝑛-Locally SConn ⊆ 𝑛-Locally Conn
7		llyssnlly	⊢ Locally SConn ⊆ 𝑛-Locally SConn
8		iillysconn	⊢ II ∈ Locally SConn
9	7 8	sselii	⊢ II ∈ 𝑛-Locally SConn
10	6 9	sselii	⊢ II ∈ 𝑛-Locally Conn