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 o. - ) |` ( ( 0 [,] 1 ) X. ( 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 o. - )
5		cc0	|- 0
6		cicc	|- [,]
7		c1	|- 1
8	5 7 6	co	|- ( 0 [,] 1 )
9	8 8	cxp	|- ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) )
10	4 9	cres	|- ( ( abs o. - ) |` ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) )
11	10 1	cfv	|- ( MetOpen ` ( ( abs o. - ) |` ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) )
12	0 11	wceq	|- II = ( MetOpen ` ( ( abs o. - ) |` ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) )