Metamath Proof Explorer


Theorem iccsconn

Description: A closed interval is simply connected. (Contributed by Mario Carneiro, 9-Mar-2015)

Ref Expression
Assertion iccsconn ABtopGenran.𝑡ABSConn

Proof

Step Hyp Ref Expression
1 iccconn ABtopGenran.𝑡ABConn
2 iccssre ABAB
3 eqid topGenran.𝑡AB=topGenran.𝑡AB
4 3 resconn ABtopGenran.𝑡ABSConntopGenran.𝑡ABConn
5 2 4 syl ABtopGenran.𝑡ABSConntopGenran.𝑡ABConn
6 1 5 mpbird ABtopGenran.𝑡ABSConn