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]\times \left[0,1\right]\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfii2	$$⊢\mathrm{II}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){\upharpoonright }_{𝑡}\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){\upharpoonright }_{𝑡}\left[0,1\right]=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){\upharpoonright }_{𝑡}\left[0,1\right]$$
6	2 5	ax-mp	$$⊢\mathrm{ordTop}\left(\le \right){\upharpoonright }_{𝑡}\left[0,1\right]=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){\upharpoonright }_{𝑡}\left[0,1\right]$$
7		ordtresticc	$$⊢\mathrm{ordTop}\left(\le \right){\upharpoonright }_{𝑡}\left[0,1\right]=\mathrm{ordTop}\left(\le \cap \left(\left[0,1\right]\times \left[0,1\right]\right)\right)$$
8	1 6 7	3eqtr2i	$$⊢\mathrm{II}=\mathrm{ordTop}\left(\le \cap \left(\left[0,1\right]\times \left[0,1\right]\right)\right)$$