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 ` <_ ) )