Definition df-ioc 11297

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 11293	. 2 class (,]
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cxr 9409	. . 3 class RR*
5	2	cv 1368	. . . . . 6 class x
6		vz	. . . . . . 7 setvar z
7	6	cv 1368	. . . . . 6 class z
8		clt 9410	. . . . . 6 class <
9	5, 7, 8	wbr 4287	. . . . 5 wff x < z
10	3	cv 1368	. . . . . 6 class y
11		cle 9411	. . . . . 6 class <_
12	7, 10, 11	wbr 4287	. . . . 5 wff z <_ y
13	9, 12	wa 369	. . . 4 wff ( x < z /\ z <_ y )
14	13, 6, 4	crab 2714	. . 3 class { z e. RR* | ( x < z /\ z <_ y ) }
15	2, 3, 4, 4, 14	cmpt2 6088	. 2 class ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )
16	1, 15	wceq 1369	1 wff (,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )

This definition is referenced by:  iocval  11329  elioc1  11334  iocssxr  11371  snunioc  11405  leordtval2  18791  iocpnfordt  18794  lecldbas  18798  pnfnei  18799  iocmnfcld  20323  xrtgioo  20358  ismbf3d  21107  dvloglem  22068  iocssicc  26010  iocssioo  26012  asindmre  28432  dvasin  28433  ioounsn  29538