Step |
Hyp |
Ref |
Expression |
1 |
|
dfii2 |
⊢ II = ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] 1 ) ) |
2 |
|
unitssre |
⊢ ( 0 [,] 1 ) ⊆ ℝ |
3 |
|
eqid |
⊢ ( ordTop ‘ ≤ ) = ( ordTop ‘ ≤ ) |
4 |
|
eqid |
⊢ ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) ) |
5 |
3 4
|
xrrest |
⊢ ( ( 0 [,] 1 ) ⊆ ℝ → ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] 1 ) ) = ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] 1 ) ) ) |
6 |
2 5
|
ax-mp |
⊢ ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] 1 ) ) = ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] 1 ) ) |
7 |
|
ordtresticc |
⊢ ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] 1 ) ) = ( ordTop ‘ ( ≤ ∩ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) ) |
8 |
1 6 7
|
3eqtr2i |
⊢ II = ( ordTop ‘ ( ≤ ∩ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) ) |