Metamath Proof Explorer

Theorem iillysconn

Description: The unit interval is locally simply connected. (Contributed by Mario Carneiro, 10-Mar-2015)

Ref Expression
Assertion iillysconn ⊢ II ∈ Locally SConn

Proof

Step Hyp Ref Expression
1 dfii2 ⊢ II = topGen ⁡ ran ⁡ . ↾ 𝑡 0 1
2 0re ⊢ 0 ∈ ℝ
3 1re ⊢ 1 ∈ ℝ
4 iccllysconn ⊢ 0 ∈ ℝ ∧ 1 ∈ ℝ → topGen ⁡ ran ⁡ . ↾ 𝑡 0 1 ∈ Locally SConn
5 2 3 4 mp2an ⊢ topGen ⁡ ran ⁡ . ↾ 𝑡 0 1 ∈ Locally SConn
6 1 5 eqeltri ⊢ II ∈ Locally SConn