# Metamath Proof Explorer

## 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)↾}_{\left(\left[0,1\right]×\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 ${class}0$
6 cicc ${class}\left[.\right]$
7 c1 ${class}1$
8 5 7 6 co ${class}\left[0,1\right]$
9 8 8 cxp ${class}\left(\left[0,1\right]×\left[0,1\right]\right)$
10 4 9 cres ${class}\left({\left(\mathrm{abs}\circ -\right)↾}_{\left(\left[0,1\right]×\left[0,1\right]\right)}\right)$
11 10 1 cfv ${class}\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)↾}_{\left(\left[0,1\right]×\left[0,1\right]\right)}\right)$
12 0 11 wceq ${wff}\mathrm{II}=\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)↾}_{\left(\left[0,1\right]×\left[0,1\right]\right)}\right)$