# Metamath Proof Explorer

## Theorem dfii5

Description: The unit interval expressed as an order topology. (Contributed by Mario Carneiro, 9-Sep-2015)

Ref Expression
Assertion dfii5 ${⊢}\mathrm{II}=\mathrm{ordTop}\left(\le \cap \left(\left[0,1\right]×\left[0,1\right]\right)\right)$

### Proof

Step Hyp Ref Expression
1 dfii2 ${⊢}\mathrm{II}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}\left[0,1\right]$
2 unitssre ${⊢}\left[0,1\right]\subseteq ℝ$
3 eqid ${⊢}\mathrm{ordTop}\left(\le \right)=\mathrm{ordTop}\left(\le \right)$
4 eqid ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
5 3 4 xrrest ${⊢}\left[0,1\right]\subseteq ℝ\to \mathrm{ordTop}\left(\le \right){↾}_{𝑡}\left[0,1\right]=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}\left[0,1\right]$
6 2 5 ax-mp ${⊢}\mathrm{ordTop}\left(\le \right){↾}_{𝑡}\left[0,1\right]=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}\left[0,1\right]$
7 ordtresticc ${⊢}\mathrm{ordTop}\left(\le \right){↾}_{𝑡}\left[0,1\right]=\mathrm{ordTop}\left(\le \cap \left(\left[0,1\right]×\left[0,1\right]\right)\right)$
8 1 6 7 3eqtr2i ${⊢}\mathrm{II}=\mathrm{ordTop}\left(\le \cap \left(\left[0,1\right]×\left[0,1\right]\right)\right)$