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 Clsd II

Proof

Step Hyp Ref Expression
1 iccssxr 0 1 *
2 iccordt A B Clsd ordTop
3 0re 0
4 1re 1
5 iccss 0 1 0 A B 1 A B 0 1
6 3 4 5 mpanl12 0 A B 1 A B 0 1
7 letopuni * = ordTop
8 7 restcldi 0 1 * A B Clsd ordTop A B 0 1 A B Clsd ordTop 𝑡 0 1
9 1 2 6 8 mp3an12i 0 A B 1 A B Clsd ordTop 𝑡 0 1
10 dfii5 II = ordTop 0 1 × 0 1
11 ordtresticc ordTop 𝑡 0 1 = ordTop 0 1 × 0 1
12 10 11 eqtr4i II = ordTop 𝑡 0 1
13 12 fveq2i Clsd II = Clsd ordTop 𝑡 0 1
14 9 13 eleqtrrdi 0 A B 1 A B Clsd II