Metamath Proof Explorer

Theorem icccldii

Description: Closed intervals are closed sets of II . Note that iccss , iccordt , and ordtresticc are proved from ixxss12 , ordtcld3 , and ordtrest2 , respectively. An alternate proof uses restcldi , dfii2 , and icccld . (Contributed by Zhi Wang, 8-Sep-2024)

Ref Expression
Assertion icccldii 
|- ( ( 0 <_ A /\ B <_ 1 ) -> ( A [,] B ) e. ( Clsd ` II ) )

Proof

Step Hyp Ref Expression
1 iccssxr 
 |-  ( 0 [,] 1 ) C_ RR*
2 iccordt 
 |-  ( A [,] B ) e. ( Clsd ` ( ordTop ` <_ ) )
3 0re 
 |-  0 e. RR
4 1re 
 |-  1 e. RR
5 iccss 
 |-  ( ( ( 0 e. RR /\ 1 e. RR ) /\ ( 0 <_ A /\ B <_ 1 ) ) -> ( A [,] B ) C_ ( 0 [,] 1 ) )
6 3 4 5 mpanl12 
 |-  ( ( 0 <_ A /\ B <_ 1 ) -> ( A [,] B ) C_ ( 0 [,] 1 ) )
7 letopuni 
 |-  RR* = U. ( ordTop ` <_ )
8 7 restcldi 
 |-  ( ( ( 0 [,] 1 ) C_ RR* /\ ( A [,] B ) e. ( Clsd ` ( ordTop ` <_ ) ) /\ ( A [,] B ) C_ ( 0 [,] 1 ) ) -> ( A [,] B ) e. ( Clsd ` ( ( ordTop ` <_ ) |`t ( 0 [,] 1 ) ) ) )
9 1 2 6 8 mp3an12i 
 |-  ( ( 0 <_ A /\ B <_ 1 ) -> ( A [,] B ) e. ( Clsd ` ( ( ordTop ` <_ ) |`t ( 0 [,] 1 ) ) ) )
10 dfii5 
 |-  II = ( ordTop ` ( <_ i^i ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) )
11 ordtresticc 
 |-  ( ( ordTop ` <_ ) |`t ( 0 [,] 1 ) ) = ( ordTop ` ( <_ i^i ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) )
12 10 11 eqtr4i 
 |-  II = ( ( ordTop ` <_ ) |`t ( 0 [,] 1 ) )
13 12 fveq2i 
 |-  ( Clsd ` II ) = ( Clsd ` ( ( ordTop ` <_ ) |`t ( 0 [,] 1 ) ) )
14 9 13 eleqtrrdi 
 |-  ( ( 0 <_ A /\ B <_ 1 ) -> ( A [,] B ) e. ( Clsd ` II ) )