Definition df-ioc 11640

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 11636	. 2 class (,]
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cxr 9673	. . 3 class RR*
5	2	cv 1436	. . . . . 6 class x
6		vz	. . . . . . 7 setvar z
7	6	cv 1436	. . . . . 6 class z
8		clt 9674	. . . . . 6 class <
9	5, 7, 8	wbr 4426	. . . . 5 wff x < z
10	3	cv 1436	. . . . . 6 class y
11		cle 9675	. . . . . 6 class <_
12	7, 10, 11	wbr 4426	. . . . 5 wff z <_ y
13	9, 12	wa 370	. . . 4 wff ( x < z /\ z <_ y )
14	13, 6, 4	crab 2786	. . 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  11673  elioc1  11678  iocssxr  11718  iocssicc  11722  iocssioo  11724  snunioc  11758  leordtval2  20159  iocpnfordt  20162  lecldbas  20166  pnfnei  20167  iocmnfcld  21700  xrtgioo  21735  ismbf3d  22487  dvloglem  23458  asindmre  31730  dvasin  31731  ioounsn  35792  ioossioc  37172  snunioo2  37190  eliocre  37193  lbioc  37198