Metamath Proof Explorer

Theorem iccordt

Description: A closed interval is closed in the order topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Assertion iccordt 
|- ( A [,] B ) e. ( Clsd ` ( ordTop ` <_ ) )

Proof

Step Hyp Ref Expression
1 df-ov 
 |-  ( A [,] B ) = ( [,] ` <. A , B >. )
2 letsr 
 |-  <_ e. TosetRel
3 ledm 
 |-  RR* = dom <_
4 3 ordtcld3 
 |-  ( ( <_ e. TosetRel /\ x e. RR* /\ y e. RR* ) -> { z e. RR* | ( x <_ z /\ z <_ y ) } e. ( Clsd ` ( ordTop ` <_ ) ) )
5 2 4 mp3an1 
 |-  ( ( x e. RR* /\ y e. RR* ) -> { z e. RR* | ( x <_ z /\ z <_ y ) } e. ( Clsd ` ( ordTop ` <_ ) ) )
6 5 rgen2 
 |-  A. x e. RR* A. y e. RR* { z e. RR* | ( x <_ z /\ z <_ y ) } e. ( Clsd ` ( ordTop ` <_ ) )
7 df-icc 
 |-  [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )
8 7 fmpo 
 |-  ( A. x e. RR* A. y e. RR* { z e. RR* | ( x <_ z /\ z <_ y ) } e. ( Clsd ` ( ordTop ` <_ ) ) <-> [,] : ( RR* X. RR* ) --> ( Clsd ` ( ordTop ` <_ ) ) )
9 6 8 mpbi 
 |-  [,] : ( RR* X. RR* ) --> ( Clsd ` ( ordTop ` <_ ) )
10 letop 
 |-  ( ordTop ` <_ ) e. Top
11 0cld 
 |-  ( ( ordTop ` <_ ) e. Top -> (/) e. ( Clsd ` ( ordTop ` <_ ) ) )
12 10 11 ax-mp 
 |-  (/) e. ( Clsd ` ( ordTop ` <_ ) )
13 9 12 f0cli 
 |-  ( [,] ` <. A , B >. ) e. ( Clsd ` ( ordTop ` <_ ) )
14 1 13 eqeltri 
 |-  ( A [,] B ) e. ( Clsd ` ( ordTop ` <_ ) )