Metamath Proof Explorer

Theorem icccld

Description: Closed intervals are closed sets of the standard topology on RR . (Contributed by FL, 14-Sep-2007)

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

Proof

Step Hyp Ref Expression
1 difreicc 
 |-  ( ( A e. RR /\ B e. RR ) -> ( RR \ ( A [,] B ) ) = ( ( -oo (,) A ) u. ( B (,) +oo ) ) )
2 retop 
 |-  ( topGen ` ran (,) ) e. Top
3 iooretop 
 |-  ( -oo (,) A ) e. ( topGen ` ran (,) )
4 iooretop 
 |-  ( B (,) +oo ) e. ( topGen ` ran (,) )
5 unopn 
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ ( -oo (,) A ) e. ( topGen ` ran (,) ) /\ ( B (,) +oo ) e. ( topGen ` ran (,) ) ) -> ( ( -oo (,) A ) u. ( B (,) +oo ) ) e. ( topGen ` ran (,) ) )
6 2 3 4 5 mp3an 
 |-  ( ( -oo (,) A ) u. ( B (,) +oo ) ) e. ( topGen ` ran (,) )
7 1 6 eqeltrdi 
 |-  ( ( A e. RR /\ B e. RR ) -> ( RR \ ( A [,] B ) ) e. ( topGen ` ran (,) ) )
8 iccssre 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
9 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
10 9 iscld2 
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ ( A [,] B ) C_ RR ) -> ( ( A [,] B ) e. ( Clsd ` ( topGen ` ran (,) ) ) <-> ( RR \ ( A [,] B ) ) e. ( topGen ` ran (,) ) ) )
11 2 8 10 sylancr 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A [,] B ) e. ( Clsd ` ( topGen ` ran (,) ) ) <-> ( RR \ ( A [,] B ) ) e. ( topGen ` ran (,) ) ) )
12 7 11 mpbird 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) e. ( Clsd ` ( topGen ` ran (,) ) ) )