Definition df-ii

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
Assertion	df-ii	⊢ II = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cii	⊢ II
1		cmopn	⊢ MetOpen
2		cabs	⊢ abs
3		cmin	⊢ −
4	2 3	ccom	⊢ ( abs ∘ − )
5		cc0	⊢ 0
6		cicc	⊢ [,]
7		c1	⊢ 1
8	5 7 6	co	⊢ ( 0 [,] 1 )
9	8 8	cxp	⊢ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) )
10	4 9	cres	⊢ ( ( abs ∘ − ) ↾ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
11	10 1	cfv	⊢ ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) )
12	0 11	wceq	⊢ II = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) )