![]() |
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 24390 | . 2 class II | |
2 | cabs 15180 | . . . . 5 class abs | |
3 | cmin 11443 | . . . . 5 class − | |
4 | 2, 3 | ccom 5680 | . . . 4 class (abs ∘ − ) |
5 | cc0 11109 | . . . . . 6 class 0 | |
6 | c1 11110 | . . . . . 6 class 1 | |
7 | cicc 13326 | . . . . . 6 class [,] | |
8 | 5, 6, 7 | co 7408 | . . . . 5 class (0[,]1) |
9 | 8, 8 | cxp 5674 | . . . 4 class ((0[,]1) × (0[,]1)) |
10 | 4, 9 | cres 5678 | . . 3 class ((abs ∘ − ) ↾ ((0[,]1) × (0[,]1))) |
11 | cmopn 20933 | . . 3 class MetOpen | |
12 | 10, 11 | cfv 6543 | . 2 class (MetOpen‘((abs ∘ − ) ↾ ((0[,]1) × (0[,]1)))) |
13 | 1, 12 | wceq 1541 | 1 wff II = (MetOpen‘((abs ∘ − ) ↾ ((0[,]1) × (0[,]1)))) |
Colors of variables: wff setvar class |
This definition is referenced by: iitopon 24394 dfii2 24397 dfii3 24398 lebnumii 24481 |
Copyright terms: Public domain | W3C validator |