Definition df-ioc 11530

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 11526	. 2 class (,]
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cxr 9623	. . 3 class RR*
5	2	cv 1378	. . . . . 6 class x
6		vz	. . . . . . 7 setvar z
7	6	cv 1378	. . . . . 6 class z
8		clt 9624	. . . . . 6 class <
9	5, 7, 8	wbr 4447	. . . . 5 wff x < z
10	3	cv 1378	. . . . . 6 class y
11		cle 9625	. . . . . 6 class <_
12	7, 10, 11	wbr 4447	. . . . 5 wff z <_ y
13	9, 12	wa 369	. . . 4 wff ( x < z /\ z <_ y )
14	13, 6, 4	crab 2818	. . 3 class { z e. RR* | ( x < z /\ z <_ y ) }
15	2, 3, 4, 4, 14	cmpt2 6284	. 2 class ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )
16	1, 15	wceq 1379	1 wff (,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )

This definition is referenced by:  iocval  11562  elioc1  11567  iocssxr  11604  iocssicc  11608  iocssioo  11610  snunioc  11644  leordtval2  19476  iocpnfordt  19479  lecldbas  19483  pnfnei  19484  iocmnfcld  21008  xrtgioo  21043  ismbf3d  21793  dvloglem  22754  asindmre  29677  dvasin  29678  ioounsn  30782  ioossioc  31088  snunioo2  31108  eliocre  31111  lbioc  31117