Definition df-icc 10879

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 10875	. 2 class [,]
2		vx	. . 3 set x
3		vy	. . 3 set y
4		cxr 9075	. . 3 class RR*
5	2	cv 1648	. . . . . 6 class x
6		vz	. . . . . . 7 set z
7	6	cv 1648	. . . . . 6 class z
8		cle 9077	. . . . . 6 class <_
9	5, 7, 8	wbr 4172	. . . . 5 wff x <_ z
10	3	cv 1648	. . . . . 6 class y
11	7, 10, 8	wbr 4172	. . . . 5 wff z <_ y
12	9, 11	wa 359	. . . 4 wff ( x <_ z /\ z <_ y )
13	12, 6, 4	crab 2670	. . 3 class { z e. RR* | ( x <_ z /\ z <_ y ) }
14	2, 3, 4, 4, 13	cmpt2 6042	. 2 class ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )
15	1, 14	wceq 1649	1 wff [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )

This definition is referenced by:  iccval  10911  elicc1  10916  iccss  10934  iccssioo  10935  iccss2  10937  iccssico  10938  iccssxr  10949  ioossicc  10952  iccf  10959  snunioo  10979  snunico  10980  ioodisj  10982  leordtval2  17230  iccordt  17232  lecldbas  17237  ioombl  19412  itg2mulclem  19591  itg2mulc  19592  itgspliticc  19681  psercnlem2  20293  tanord1  20392  icossicc  24082  iocssicc  24083  snunioc  24090  cvmliftlem10  24934