Metamath Proof Explorer

Theorem retopconn

Description: Corollary of reconn . The set of real numbers is connected. (Contributed by Jeff Hankins, 17-Aug-2009)

Ref Expression
Assertion retopconn 
|- ( topGen ` ran (,) ) e. Conn

Proof

Step Hyp Ref Expression
1 retop 
 |-  ( topGen ` ran (,) ) e. Top
2 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
3 2 restid 
 |-  ( ( topGen ` ran (,) ) e. Top -> ( ( topGen ` ran (,) ) |`t RR ) = ( topGen ` ran (,) ) )
4 1 3 ax-mp 
 |-  ( ( topGen ` ran (,) ) |`t RR ) = ( topGen ` ran (,) )
5 iccssre 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x [,] y ) C_ RR )
6 5 rgen2 
 |-  A. x e. RR A. y e. RR ( x [,] y ) C_ RR
7 ssid 
 |-  RR C_ RR
8 reconn 
 |-  ( RR C_ RR -> ( ( ( topGen ` ran (,) ) |`t RR ) e. Conn <-> A. x e. RR A. y e. RR ( x [,] y ) C_ RR ) )
9 7 8 ax-mp 
 |-  ( ( ( topGen ` ran (,) ) |`t RR ) e. Conn <-> A. x e. RR A. y e. RR ( x [,] y ) C_ RR )
10 6 9 mpbir 
 |-  ( ( topGen ` ran (,) ) |`t RR ) e. Conn
11 4 10 eqeltrri 
 |-  ( topGen ` ran (,) ) e. Conn