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 ) ) ) ) |
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 ) ) ) ) |