Definition df-ioc 11630

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 11626	. 2 class (,]
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cxr 9661	. . 3 class RR*
5	2	cv 1447	. . . . . 6 class x
6		vz	. . . . . . 7 setvar z
7	6	cv 1447	. . . . . 6 class z
8		clt 9662	. . . . . 6 class <
9	5, 7, 8	wbr 4374	. . . . 5 wff x < z
10	3	cv 1447	. . . . . 6 class y
11		cle 9663	. . . . . 6 class <_
12	7, 10, 11	wbr 4374	. . . . 5 wff z <_ y
13	9, 12	wa 375	. . . 4 wff ( x < z /\ z <_ y )
14	13, 6, 4	crab 2741	. . 3 class { z e. RR* | ( x < z /\ z <_ y ) }
15	2, 3, 4, 4, 14	cmpt2 6278	. 2 class ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )
16	1, 15	wceq 1448	1 wff (,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )

This definition is referenced by:  iocval  11663  elioc1  11668  iocssxr  11708  iocssicc  11712  iocssioo  11714  snunioc  11751  leordtval2  20239  iocpnfordt  20242  lecldbas  20246  pnfnei  20247  iocmnfcld  21800  xrtgioo  21835  ismbf3d  22622  dvloglem  23605  asindmre  32029  dvasin  32030  ioounsn  36096  ioossioc  37629  snunioo2  37647  eliocre  37650  lbioc  37655