Definition df-ii 16690

Description: Define the unit interval with the Euclidean topology.

Assertion

Ref	Expression
df-ii	|- II = (MetOpen` ((abs o. - ) |` ((0[,]1) X. (0[,]1))))

Detailed syntax breakdown of Definition df-ii

Step	Hyp	Ref	Expression
1		cii 16689	. 2 class II
2		cabs 8384	. . . . 5 class abs
3		cmin 6989	. . . . 5 class -
4	2, 3	ccom 4123	. . . 4 class (abs o. - )
5		cc0 6752	. . . . . 6 class 0
6		c1 6753	. . . . . 6 class 1
7		cicc 7873	. . . . . 6 class [,]
8	5, 6, 7	co 4981	. . . . 5 class (0[,]1)
9	8, 8	cxp 4117	. . . 4 class ((0[,]1) X. (0[,]1))
10	4, 9	cres 4121	. . 3 class ((abs o. - ) |` ((0[,]1) X. (0[,]1)))
11		copn 9935	. . 3 class MetOpen
12	10, 11	cfv 4131	. 2 class (MetOpen` ((abs o. - ) |` ((0[,]1) X. (0[,]1))))
13	1, 12	wceq 1586	1 wff II = (MetOpen` ((abs o. - ) |` ((0[,]1) X. (0[,]1))))

This definition is referenced by:  iitop 16691  iiuni 16692  dfii2 16693  dfii3 16694  iicmp 16852  phtpycom 16874  phtpycolem3 16877  phtpycolem4 16878  pcocn 16900  pcohtpylem3 16906  pcopt 16908  pcoass 16909  pcorev 16911  pi1gp 16919

Copyright terms: Public domain