Definition df-ii

Description: Define the unit interval with the Euclidean topology. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 3-Sep-2015)

	Ref	Expression
Assertion	df-ii	$$⊢\mathrm{II}=\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(\left[0,1\right]\times \left[0,1\right]\right)}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cii	$$class\mathrm{II}$$
1		cmopn	$$class\mathrm{MetOpen}$$
2		cabs	$$class\mathrm{abs}$$
3		cmin	$$class-$$
4	2 3	ccom	$$class\left(\mathrm{abs}\circ -\right)$$
5		cc0	$$class0$$
6		cicc	$$class\left[.\right]$$
7		c1	$$class1$$
8	5 7 6	co	$$class\left[0,1\right]$$
9	8 8	cxp	$$class\left(\left[0,1\right]\times \left[0,1\right]\right)$$
10	4 9	cres	$$class\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(\left[0,1\right]\times \left[0,1\right]\right)}\right)$$
11	10 1	cfv	$$class\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(\left[0,1\right]\times \left[0,1\right]\right)}\right)$$
12	0 11	wceq	$$wff\mathrm{II}=\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(\left[0,1\right]\times \left[0,1\right]\right)}\right)$$