Definition df-ioc 12180

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 12176	. 2 class (,]
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cxr 10073	. . 3 class RR*
5	2	cv 1482	. . . . . 6 class x
6		vz	. . . . . . 7 setvar z
7	6	cv 1482	. . . . . 6 class z
8		clt 10074	. . . . . 6 class <
9	5, 7, 8	wbr 4653	. . . . 5 wff x < z
10	3	cv 1482	. . . . . 6 class y
11		cle 10075	. . . . . 6 class <_
12	7, 10, 11	wbr 4653	. . . . 5 wff z <_ y
13	9, 12	wa 384	. . . 4 wff ( x < z /\ z <_ y )
14	13, 6, 4	crab 2916	. . 3 class { z e. RR* | ( x < z /\ z <_ y ) }
15	2, 3, 4, 4, 14	cmpt2 6652	. 2 class ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )
16	1, 15	wceq 1483	1 wff (,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )

This definition is referenced by:  iocval  12212  elioc1  12217  iocssxr  12257  iocssicc  12261  iocssioo  12263  snunioc  12300  leordtval2  21016  iocpnfordt  21019  lecldbas  21023  pnfnei  21024  iocmnfcld  22572  xrtgioo  22609  ismbf3d  23421  dvloglem  24394  asindmre  33495  dvasin  33496  ioounsn  37795  ioossioc  39713  snunioo2  39731  eliocre  39734  lbioc  39739