Definition df-ioc 11406

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 11402	. 2 class (,]
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cxr 9518	. . 3 class RR*
5	2	cv 1369	. . . . . 6 class x
6		vz	. . . . . . 7 setvar z
7	6	cv 1369	. . . . . 6 class z
8		clt 9519	. . . . . 6 class <
9	5, 7, 8	wbr 4390	. . . . 5 wff x < z
10	3	cv 1369	. . . . . 6 class y
11		cle 9520	. . . . . 6 class <_
12	7, 10, 11	wbr 4390	. . . . 5 wff z <_ y
13	9, 12	wa 369	. . . 4 wff ( x < z /\ z <_ y )
14	13, 6, 4	crab 2799	. . 3 class { z e. RR* | ( x < z /\ z <_ y ) }
15	2, 3, 4, 4, 14	cmpt2 6192	. 2 class ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )
16	1, 15	wceq 1370	1 wff (,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )

This definition is referenced by:  iocval  11438  elioc1  11443  iocssxr  11480  snunioc  11514  leordtval2  18932  iocpnfordt  18935  lecldbas  18939  pnfnei  18940  iocmnfcld  20464  xrtgioo  20499  ismbf3d  21248  dvloglem  22209  iocssicc  26193  iocssioo  26195  asindmre  28617  dvasin  28618  ioounsn  29723