HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Definition df-ii 12952
Description: Define the unit interval with the Euclidean topology.
Assertion
Ref Expression
df-ii

Detailed syntax breakdown of Definition df-ii
StepHypRef Expression
1 cii 12951 . 2
2 cabs 9360 . . . . 5
3 cmin 7487 . . . . 5
42, 3ccom 4038 . . . 4
5 cc0 7257 . . . . . 6
6 c1 7258 . . . . . 6
7 cicc 8659 . . . . . 6
85, 6, 7co 5032 . . . . 5
98, 8cxp 4032 . . . 4
104, 9cres 4036 . . 3
11 copn 12760 . . 3
1210, 11cfv 4046 . 2
131, 12wceq 1414 1
Colors of variables: wff set class
This definition is referenced by:  iitop 12953  iiuni 12954  dfii2 12955  dfii3 12956  lebnumii 12984
Copyright terms: Public domain