Definition df-ioc

Description: Define the set of open-below, closed-above intervals of extended reals. (Contributed by NM, 24-Dec-2006)

	Ref	Expression
Assertion	df-ioc	|- (,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cioc	|- (,]
1		vx	|- x
2		cxr	|- RR*
3		vy	|- y
4		vz	|- z
5	1	cv	|- x
6		clt	|- <
7	4	cv	|- z
8	5 7 6	wbr	|- x < z
9		cle	|- <_
10	3	cv	|- y
11	7 10 9	wbr	|- z <_ y
12	8 11	wa	|- ( x < z /\ z <_ y )
13	12 4 2	crab	|- { z e. RR* | ( x < z /\ z <_ y ) }
14	1 3 2 2 13	cmpo	|- ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )
15	0 14	wceq	|- (,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )