Metamath Proof Explorer

Theorem retopsconn

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

Ref Expression
Assertion retopsconn 
|- ( topGen ` ran (,) ) e. SConn

Proof

Step Hyp Ref Expression
1 retop 
 |-  ( topGen ` ran (,) ) e. Top
2 ioomax 
 |-  ( -oo (,) +oo ) = RR
3 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
4 2 3 eqtri 
 |-  ( -oo (,) +oo ) = U. ( topGen ` ran (,) )
5 4 restid 
 |-  ( ( topGen ` ran (,) ) e. Top -> ( ( topGen ` ran (,) ) |`t ( -oo (,) +oo ) ) = ( topGen ` ran (,) ) )
6 1 5 ax-mp 
 |-  ( ( topGen ` ran (,) ) |`t ( -oo (,) +oo ) ) = ( topGen ` ran (,) )
7 ioosconn 
 |-  ( ( topGen ` ran (,) ) |`t ( -oo (,) +oo ) ) e. SConn
8 6 7 eqeltrri 
 |-  ( topGen ` ran (,) ) e. SConn