Metamath Proof Explorer


Theorem iillysconn

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

Ref Expression
Assertion iillysconn IILocally SConn

Proof

Step Hyp Ref Expression
1 dfii2 II=topGenran.𝑡01
2 0re 0
3 1re 1
4 iccllysconn 01topGenran.𝑡01Locally SConn
5 2 3 4 mp2an topGenran.𝑡01Locally SConn
6 1 5 eqeltri IILocally SConn