Definition df-icc 11667

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 11663	. 2 class [,]
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cxr 9692	. . 3 class RR*
5	2	cv 1451	. . . . . 6 class x
6		vz	. . . . . . 7 setvar z
7	6	cv 1451	. . . . . 6 class z
8		cle 9694	. . . . . 6 class <_
9	5, 7, 8	wbr 4395	. . . . 5 wff x <_ z
10	3	cv 1451	. . . . . 6 class y
11	7, 10, 8	wbr 4395	. . . . 5 wff z <_ y
12	9, 11	wa 376	. . . 4 wff ( x <_ z /\ z <_ y )
13	12, 6, 4	crab 2760	. . 3 class { z e. RR* | ( x <_ z /\ z <_ y ) }
14	2, 3, 4, 4, 13	cmpt2 6310	. 2 class ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )
15	1, 14	wceq 1452	1 wff [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )

This definition is referenced by:  iccval  11700  elicc1  11705  iccss  11727  iccssioo  11728  iccss2  11730  iccssico  11731  iccssxr  11742  ioossicc  11745  icossicc  11746  iocssicc  11747  iccf  11758  snunioo  11784  snunico  11785  snunioc  11786  ioodisj  11788  leordtval2  20305  iccordt  20307  lecldbas  20312  ioombl  22597  itgspliticc  22873  psercnlem2  23458  tanord1  23565  cvmliftlem10  30089  ftc1anclem7  32087  ftc1anclem8  32088  ftc1anc  32089  ioounsn  36165  snunioo2  37702  snunioo1  37709