![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-ii | Structured version Visualization version GIF version |
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 |
---|---|
df-ii | ⊢ II = (MetOpen‘((abs ∘ − ) ↾ ((0[,]1) × (0[,]1)))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cii 24391 | . 2 class II | |
2 | cabs 15181 | . . . . 5 class abs | |
3 | cmin 11444 | . . . . 5 class − | |
4 | 2, 3 | ccom 5681 | . . . 4 class (abs ∘ − ) |
5 | cc0 11110 | . . . . . 6 class 0 | |
6 | c1 11111 | . . . . . 6 class 1 | |
7 | cicc 13327 | . . . . . 6 class [,] | |
8 | 5, 6, 7 | co 7409 | . . . . 5 class (0[,]1) |
9 | 8, 8 | cxp 5675 | . . . 4 class ((0[,]1) × (0[,]1)) |
10 | 4, 9 | cres 5679 | . . 3 class ((abs ∘ − ) ↾ ((0[,]1) × (0[,]1))) |
11 | cmopn 20934 | . . 3 class MetOpen | |
12 | 10, 11 | cfv 6544 | . 2 class (MetOpen‘((abs ∘ − ) ↾ ((0[,]1) × (0[,]1)))) |
13 | 1, 12 | wceq 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 |