Definition df-icc 11299

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 11295	. 2 class [,]
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cxr 9409	. . 3 class RR*
5	2	cv 1368	. . . . . 6 class x
6		vz	. . . . . . 7 setvar z
7	6	cv 1368	. . . . . 6 class z
8		cle 9411	. . . . . 6 class <_
9	5, 7, 8	wbr 4287	. . . . 5 wff x <_ z
10	3	cv 1368	. . . . . 6 class y
11	7, 10, 8	wbr 4287	. . . . 5 wff z <_ y
12	9, 11	wa 369	. . . 4 wff ( x <_ z /\ z <_ y )
13	12, 6, 4	crab 2714	. . 3 class { z e. RR* | ( x <_ z /\ z <_ y ) }
14	2, 3, 4, 4, 13	cmpt2 6088	. 2 class ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )
15	1, 14	wceq 1369	1 wff [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )

This definition is referenced by:  iccval  11331  elicc1  11336  iccss  11355  iccssioo  11356  iccss2  11358  iccssico  11359  iccssxr  11370  ioossicc  11373  iccf  11380  snunioo  11403  snunico  11404  snunioc  11405  ioodisj  11407  leordtval2  18791  iccordt  18793  lecldbas  18798  ioombl  21021  itg2mulclem  21199  itg2mulc  21200  itgspliticc  21289  psercnlem2  21864  tanord1  21968  icossicc  26009  iocssicc  26010  cvmliftlem10  27135  ftc1anclem7  28426  ftc1anclem8  28427  ftc1anc  28428  ioounsn  29538