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 ≤ 𝐴𝐵 ≤ 1 ) → ( 𝐴 [,] 𝐵 ) ∈ ( Clsd ‘ II ) )

Proof

Step Hyp Ref Expression
1 iccssxr ( 0 [,] 1 ) ⊆ ℝ*
2 iccordt ( 𝐴 [,] 𝐵 ) ∈ ( Clsd ‘ ( ordTop ‘ ≤ ) )
3 0re 0 ∈ ℝ
4 1re 1 ∈ ℝ
5 iccss ( ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ) ∧ ( 0 ≤ 𝐴𝐵 ≤ 1 ) ) → ( 𝐴 [,] 𝐵 ) ⊆ ( 0 [,] 1 ) )
6 3 4 5 mpanl12 ( ( 0 ≤ 𝐴𝐵 ≤ 1 ) → ( 𝐴 [,] 𝐵 ) ⊆ ( 0 [,] 1 ) )
7 letopuni * = ( ordTop ‘ ≤ )
8 7 restcldi ( ( ( 0 [,] 1 ) ⊆ ℝ* ∧ ( 𝐴 [,] 𝐵 ) ∈ ( Clsd ‘ ( ordTop ‘ ≤ ) ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ( 0 [,] 1 ) ) → ( 𝐴 [,] 𝐵 ) ∈ ( Clsd ‘ ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] 1 ) ) ) )
9 1 2 6 8 mp3an12i ( ( 0 ≤ 𝐴𝐵 ≤ 1 ) → ( 𝐴 [,] 𝐵 ) ∈ ( Clsd ‘ ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] 1 ) ) ) )
10 dfii5 II = ( ordTop ‘ ( ≤ ∩ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) )
11 ordtresticc ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] 1 ) ) = ( ordTop ‘ ( ≤ ∩ ( ( 0 [,] 1 ) × ( 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 ≤ 𝐴𝐵 ≤ 1 ) → ( 𝐴 [,] 𝐵 ) ∈ ( Clsd ‘ II ) )