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