Definition df-ioc 11647

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 11643	. 2 class (,]
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cxr 9681	. . 3 class RR*
5	2	cv 1436	. . . . . 6 class x
6		vz	. . . . . . 7 setvar z
7	6	cv 1436	. . . . . 6 class z
8		clt 9682	. . . . . 6 class <
9	5, 7, 8	wbr 4423	. . . . 5 wff x < z
10	3	cv 1436	. . . . . 6 class y
11		cle 9683	. . . . . 6 class <_
12	7, 10, 11	wbr 4423	. . . . 5 wff z <_ y
13	9, 12	wa 370	. . . 4 wff ( x < z /\ z <_ y )
14	13, 6, 4	crab 2775	. . 3 class { z e. RR* | ( x < z /\ z <_ y ) }
15	2, 3, 4, 4, 14	cmpt2 6307	. 2 class ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )
16	1, 15	wceq 1437	1 wff (,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )

This definition is referenced by:  iocval  11680  elioc1  11685  iocssxr  11725  iocssicc  11729  iocssioo  11731  snunioc  11767  leordtval2  20226  iocpnfordt  20229  lecldbas  20233  pnfnei  20234  iocmnfcld  21787  xrtgioo  21822  ismbf3d  22608  dvloglem  23591  asindmre  31991  dvasin  31992  ioounsn  36064  ioossioc  37537  snunioo2  37555  eliocre  37558  lbioc  37563