Definition df-icc 11589

Description: Define the set of closed intervals of extended reals. (Contributed by NM, 24-Dec-2006.)

Assertion

Ref	Expression
df-icc	|- [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )

Distinct variable group:   x, y, z

Detailed syntax breakdown of Definition df-icc

Step	Hyp	Ref	Expression
1		cicc 11585	. 2 class [,]
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cxr 9657	. . 3 class RR*
5	2	cv 1404	. . . . . 6 class x
6		vz	. . . . . . 7 setvar z
7	6	cv 1404	. . . . . 6 class z
8		cle 9659	. . . . . 6 class <_
9	5, 7, 8	wbr 4395	. . . . 5 wff x <_ z
10	3	cv 1404	. . . . . 6 class y
11	7, 10, 8	wbr 4395	. . . . 5 wff z <_ y
12	9, 11	wa 367	. . . 4 wff ( x <_ z /\ z <_ y )
13	12, 6, 4	crab 2758	. . 3 class { z e. RR* | ( x <_ z /\ z <_ y ) }
14	2, 3, 4, 4, 13	cmpt2 6280	. 2 class ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )
15	1, 14	wceq 1405	1 wff [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )

This definition is referenced by:  iccval  11621  elicc1  11626  iccss  11646  iccssioo  11647  iccss2  11649  iccssico  11650  iccssxr  11661  ioossicc  11664  icossicc  11665  iocssicc  11666  iccf  11677  snunioo  11700  snunico  11701  snunioc  11702  ioodisj  11704  leordtval2  20006  iccordt  20008  lecldbas  20013  ioombl  22267  itgspliticc  22535  psercnlem2  23111  tanord1  23216  cvmliftlem10  29591  ftc1anclem7  31469  ftc1anclem8  31470  ftc1anc  31471  ioounsn  35541  snunioo2  36912  snunioo1  36920