Metamath Proof Explorer


Theorem ioosconn

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

Ref Expression
Assertion ioosconn topGenran.𝑡ABSConn

Proof

Step Hyp Ref Expression
1 iccssioo2 xAByABxyAB
2 1 rgen2 xAByABxyAB
3 ioossre AB
4 eqid topGenran.𝑡AB=topGenran.𝑡AB
5 4 resconn ABtopGenran.𝑡ABSConntopGenran.𝑡ABConn
6 reconn ABtopGenran.𝑡ABConnxAByABxyAB
7 5 6 bitr2d ABxAByABxyABtopGenran.𝑡ABSConn
8 3 7 ax-mp xAByABxyABtopGenran.𝑡ABSConn
9 2 8 mpbi topGenran.𝑡ABSConn