Definition df-ioc 11293

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 11289	. 2 class (,]
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cxr 9405	. . 3 class RR*
5	2	cv 1361	. . . . . 6 class x
6		vz	. . . . . . 7 setvar z
7	6	cv 1361	. . . . . 6 class z
8		clt 9406	. . . . . 6 class <
9	5, 7, 8	wbr 4280	. . . . 5 wff x < z
10	3	cv 1361	. . . . . 6 class y
11		cle 9407	. . . . . 6 class <_
12	7, 10, 11	wbr 4280	. . . . 5 wff z <_ y
13	9, 12	wa 369	. . . 4 wff ( x < z /\ z <_ y )
14	13, 6, 4	crab 2709	. . 3 class { z e. RR* | ( x < z /\ z <_ y ) }
15	2, 3, 4, 4, 14	cmpt2 6082	. 2 class ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )
16	1, 15	wceq 1362	1 wff (,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )

This definition is referenced by:  iocval  11325  elioc1  11330  iocssxr  11367  snunioc  11400  leordtval2  18658  iocpnfordt  18661  lecldbas  18665  pnfnei  18666  iocmnfcld  20190  xrtgioo  20225  ismbf3d  20974  dvloglem  21978  iocssicc  25882  iocssioo  25884  asindmre  28323  dvasin  28324  ioounsn  29430