Metamath Proof Explorer


Theorem retopsconn

Description: The real numbers are simply connected. (Contributed by Mario Carneiro, 9-Mar-2015)

Ref Expression
Assertion retopsconn topGenran.SConn

Proof

Step Hyp Ref Expression
1 retop topGenran.Top
2 ioomax −∞+∞=
3 uniretop =topGenran.
4 2 3 eqtri −∞+∞=topGenran.
5 4 restid topGenran.ToptopGenran.𝑡−∞+∞=topGenran.
6 1 5 ax-mp topGenran.𝑡−∞+∞=topGenran.
7 ioosconn topGenran.𝑡−∞+∞SConn
8 6 7 eqeltrri topGenran.SConn