Metamath Proof Explorer

Theorem ioosconn

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

Ref Expression
Assertion ioosconn 
|- ( ( topGen ` ran (,) ) |`t ( A (,) B ) ) e. SConn

Proof

Step Hyp Ref Expression
1 iccssioo2 
 |-  ( ( x e. ( A (,) B ) /\ y e. ( A (,) B ) ) -> ( x [,] y ) C_ ( A (,) B ) )
2 1 rgen2 
 |-  A. x e. ( A (,) B ) A. y e. ( A (,) B ) ( x [,] y ) C_ ( A (,) B )
3 ioossre 
 |-  ( A (,) B ) C_ RR
4 eqid 
 |-  ( ( topGen ` ran (,) ) |`t ( A (,) B ) ) = ( ( topGen ` ran (,) ) |`t ( A (,) B ) )
5 4 resconn 
 |-  ( ( A (,) B ) C_ RR -> ( ( ( topGen ` ran (,) ) |`t ( A (,) B ) ) e. SConn <-> ( ( topGen ` ran (,) ) |`t ( A (,) B ) ) e. Conn ) )
6 reconn 
 |-  ( ( A (,) B ) C_ RR -> ( ( ( topGen ` ran (,) ) |`t ( A (,) B ) ) e. Conn <-> A. x e. ( A (,) B ) A. y e. ( A (,) B ) ( x [,] y ) C_ ( A (,) B ) ) )
7 5 6 bitr2d 
 |-  ( ( A (,) B ) C_ RR -> ( A. x e. ( A (,) B ) A. y e. ( A (,) B ) ( x [,] y ) C_ ( A (,) B ) <-> ( ( topGen ` ran (,) ) |`t ( A (,) B ) ) e. SConn ) )
8 3 7 ax-mp 
 |-  ( A. x e. ( A (,) B ) A. y e. ( A (,) B ) ( x [,] y ) C_ ( A (,) B ) <-> ( ( topGen ` ran (,) ) |`t ( A (,) B ) ) e. SConn )
9 2 8 mpbi 
 |-  ( ( topGen ` ran (,) ) |`t ( A (,) B ) ) e. SConn