MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ii Structured version   Visualization version   Unicode version
Definition df-ii 22680
Description: Define the unit interval with the Euclidean topology. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 3-Sep-2015.)
Assertion
Ref Expression
df-ii |- II = ( MetOpen ` ( ( abs o. - ) |` ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) )
Detailed syntax breakdown of Definition df-ii
StepHypRef Expression
1 cii 22678 . 2 class II
2 cabs 13974 . . . . 5 class abs
3 cmin 10266 . . . . 5 class -
42, 3ccom 5118 . . . 4 class ( abs o. - )
5 cc0 9936 . . . . . 6 class 0
6 c1 9937 . . . . . 6 class 1
7 cicc 12178 . . . . . 6 class [,]
85, 6, 7co 6650 . . . . 5 class ( 0 [,] 1 )
98, 8cxp 5112 . . . 4 class ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) )
104, 9cres 5116 . . 3 class ( ( abs o. - ) |` ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) )
11 cmopn 19736 . . 3 class MetOpen
1210, 11cfv 5888 . 2 class ( MetOpen ` ( ( abs o. - ) |` ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) )
131, 12wceq 1483 1 wff II = ( MetOpen ` ( ( abs o. - ) |` ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  iitopon  22682  dfii2  22685  dfii3  22686  lebnumii  22765
  Copyright terms: Public domain W3C validator