MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ii Structured version   Unicode version

Definition df-ii 20433
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 20431 . 2  class  II
2 cabs 12715 . . . . 5  class  abs
3 cmin 9587 . . . . 5  class  -
42, 3ccom 4839 . . . 4  class  ( abs 
o.  -  )
5 cc0 9274 . . . . . 6  class  0
6 c1 9275 . . . . . 6  class  1
7 cicc 11295 . . . . . 6  class  [,]
85, 6, 7co 6086 . . . . 5  class  ( 0 [,] 1 )
98, 8cxp 4833 . . . 4  class  ( ( 0 [,] 1 )  X.  ( 0 [,] 1 ) )
104, 9cres 4837 . . 3  class  ( ( abs  o.  -  )  |`  ( ( 0 [,] 1 )  X.  (
0 [,] 1 ) ) )
11 cmopn 17786 . . 3  class  MetOpen
1210, 11cfv 5413 . 2  class  ( MetOpen `  ( ( abs  o.  -  )  |`  ( ( 0 [,] 1 )  X.  ( 0 [,] 1 ) ) ) )
131, 12wceq 1369 1  wff  II  =  ( MetOpen `  ( ( abs  o.  -  )  |`  ( ( 0 [,] 1 )  X.  (
0 [,] 1 ) ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  iitopon  20435  dfii2  20438  dfii3  20439  lebnumii  20518
  Copyright terms: Public domain W3C validator