Definition df-ii 24049

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

Step	Hyp	Ref	Expression
1		cii 24047	. 2 class II
2		cabs 14954	. . . . 5 class abs
3		cmin 11214	. . . . 5 class −
4	2, 3	ccom 5594	. . . 4 class (abs ∘ − )
5		cc0 10880	. . . . . 6 class 0
6		c1 10881	. . . . . 6 class 1
7		cicc 13091	. . . . . 6 class [,]
8	5, 6, 7	co 7284	. . . . 5 class (0[,]1)
9	8, 8	cxp 5588	. . . 4 class ((0[,]1) × (0[,]1))
10	4, 9	cres 5592	. . 3 class ((abs ∘ − ) ↾ ((0[,]1) × (0[,]1)))
11		cmopn 20596	. . 3 class MetOpen
12	10, 11	cfv 6437	. 2 class (MetOpen‘((abs ∘ − ) ↾ ((0[,]1) × (0[,]1))))
13	1, 12	wceq 1539	1 wff II = (MetOpen‘((abs ∘ − ) ↾ ((0[,]1) × (0[,]1))))

This definition is referenced by:  iitopon  24051  dfii2  24054  dfii3  24055  lebnumii  24138