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
|- II = ( MetOpen ` ( ( abs o. - ) |` ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cii
 |-  II
1 cmopn
 |-  MetOpen
2 cabs
 |-  abs
3 cmin
 |-  -
4 2 3 ccom
 |-  ( abs o. - )
5 cc0
 |-  0
6 cicc
 |-  [,]
7 c1
 |-  1
8 5 7 6 co
 |-  ( 0 [,] 1 )
9 8 8 cxp
 |-  ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) )
10 4 9 cres
 |-  ( ( abs o. - ) |` ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) )
11 10 1 cfv
 |-  ( MetOpen ` ( ( abs o. - ) |` ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) )
12 0 11 wceq
 |-  II = ( MetOpen ` ( ( abs o. - ) |` ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) )