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

Definition df-ii 24393
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 ∘ − ) ↾ ((0[,]1) × (0[,]1))))

Detailed syntax breakdown of Definition df-ii
StepHypRef Expression
1 cii 24391 . 2 class II
2 cabs 15181 . . . . 5 class abs
3 cmin 11444 . . . . 5 class
42, 3ccom 5681 . . . 4 class (abs ∘ − )
5 cc0 11110 . . . . . 6 class 0
6 c1 11111 . . . . . 6 class 1
7 cicc 13327 . . . . . 6 class [,]
85, 6, 7co 7409 . . . . 5 class (0[,]1)
98, 8cxp 5675 . . . 4 class ((0[,]1) × (0[,]1))
104, 9cres 5679 . . 3 class ((abs ∘ − ) ↾ ((0[,]1) × (0[,]1)))
11 cmopn 20934 . . 3 class MetOpen
1210, 11cfv 6544 . 2 class (MetOpen‘((abs ∘ − ) ↾ ((0[,]1) × (0[,]1))))
131, 12wceq 1542 1 wff II = (MetOpen‘((abs ∘ − ) ↾ ((0[,]1) × (0[,]1))))
Colors of variables: wff setvar class
This definition is referenced by:  iitopon  24395  dfii2  24398  dfii3  24399  lebnumii  24482
  Copyright terms: Public domain W3C validator