Metamath Proof Explorer

Theorem iccconn

Description: A closed interval is connected. (Contributed by Jeff Hankins, 17-Aug-2009)

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

Proof

Step Hyp Ref Expression
1 iccss2 
 |-  ( ( 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 iccssre 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
4 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 ) ) )
5 3 4 syl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) e. Conn <-> A. x e. ( A [,] B ) A. y e. ( A [,] B ) ( x [,] y ) C_ ( A [,] B ) ) )
6 2 5 mpbiri 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) e. Conn )