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