Definition df-icc 11644

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 11640	. 2 class [,]
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cxr 9676	. . 3 class RR*
5	2	cv 1437	. . . . . 6 class x
6		vz	. . . . . . 7 setvar z
7	6	cv 1437	. . . . . 6 class z
8		cle 9678	. . . . . 6 class <_
9	5, 7, 8	wbr 4421	. . . . 5 wff x <_ z
10	3	cv 1437	. . . . . 6 class y
11	7, 10, 8	wbr 4421	. . . . 5 wff z <_ y
12	9, 11	wa 371	. . . 4 wff ( x <_ z /\ z <_ y )
13	12, 6, 4	crab 2780	. . 3 class { z e. RR* | ( x <_ z /\ z <_ y ) }
14	2, 3, 4, 4, 13	cmpt2 6305	. 2 class ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )
15	1, 14	wceq 1438	1 wff [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )

This definition is referenced by:  iccval  11677  elicc1  11682  iccss  11704  iccssioo  11705  iccss2  11707  iccssico  11708  iccssxr  11719  ioossicc  11722  icossicc  11723  iocssicc  11724  iccf  11735  snunioo  11760  snunico  11761  snunioc  11762  ioodisj  11764  leordtval2  20220  iccordt  20222  lecldbas  20227  ioombl  22510  itgspliticc  22786  psercnlem2  23371  tanord1  23478  cvmliftlem10  30019  ftc1anclem7  31981  ftc1anclem8  31982  ftc1anc  31983  ioounsn  36058  snunioo2  37481  snunioo1  37488