Definition df-ioc 11545

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 11541	. 2 class (,]
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cxr 9630	. . 3 class RR*
5	2	cv 1382	. . . . . 6 class x
6		vz	. . . . . . 7 setvar z
7	6	cv 1382	. . . . . 6 class z
8		clt 9631	. . . . . 6 class <
9	5, 7, 8	wbr 4437	. . . . 5 wff x < z
10	3	cv 1382	. . . . . 6 class y
11		cle 9632	. . . . . 6 class <_
12	7, 10, 11	wbr 4437	. . . . 5 wff z <_ y
13	9, 12	wa 369	. . . 4 wff ( x < z /\ z <_ y )
14	13, 6, 4	crab 2797	. . 3 class { z e. RR* | ( x < z /\ z <_ y ) }
15	2, 3, 4, 4, 14	cmpt2 6283	. 2 class ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )
16	1, 15	wceq 1383	1 wff (,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )

This definition is referenced by:  iocval  11577  elioc1  11582  iocssxr  11619  iocssicc  11623  iocssioo  11625  snunioc  11659  leordtval2  19691  iocpnfordt  19694  lecldbas  19698  pnfnei  19699  iocmnfcld  21254  xrtgioo  21289  ismbf3d  22039  dvloglem  23007  asindmre  30078  dvasin  30079  ioounsn  31153  ioossioc  31478  snunioo2  31498  eliocre  31501  lbioc  31507