Metamath Proof Explorer

Theorem iccsconn

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

Ref Expression
Assertion iccsconn 
|- ( ( A e. RR /\ B e. RR ) -> ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) e. SConn )

Proof

Step Hyp Ref Expression
1 iccconn 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) e. Conn )
2 iccssre 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
3 eqid 
 |-  ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) = ( ( topGen ` ran (,) ) |`t ( A [,] B ) )
4 3 resconn 
 |-  ( ( A [,] B ) C_ RR -> ( ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) e. SConn <-> ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) e. Conn ) )
5 2 4 syl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) e. SConn <-> ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) e. Conn ) )
6 1 5 mpbird 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) e. SConn )