Definition df-ioc 11455

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

Assertion

Ref	Expression
df-ioc	|- (,] = ( 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-ioc

Step	Hyp	Ref	Expression
1		cioc 11451	. 2 class (,]
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cxr 9538	. . 3 class RR*
5	2	cv 1398	. . . . . 6 class x
6		vz	. . . . . . 7 setvar z
7	6	cv 1398	. . . . . 6 class z
8		clt 9539	. . . . . 6 class <
9	5, 7, 8	wbr 4367	. . . . 5 wff x < z
10	3	cv 1398	. . . . . 6 class y
11		cle 9540	. . . . . 6 class <_
12	7, 10, 11	wbr 4367	. . . . 5 wff z <_ y
13	9, 12	wa 367	. . . 4 wff ( x < z /\ z <_ y )
14	13, 6, 4	crab 2736	. . 3 class { z e. RR* | ( x < z /\ z <_ y ) }
15	2, 3, 4, 4, 14	cmpt2 6198	. 2 class ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )
16	1, 15	wceq 1399	1 wff (,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )

This definition is referenced by:  iocval  11487  elioc1  11492  iocssxr  11529  iocssicc  11533  iocssioo  11535  snunioc  11569  leordtval2  19799  iocpnfordt  19802  lecldbas  19806  pnfnei  19807  iocmnfcld  21361  xrtgioo  21396  ismbf3d  22146  dvloglem  23116  asindmre  30268  dvasin  30269  ioounsn  31345  ioossioc  31690  snunioo2  31710  eliocre  31713  lbioc  31719