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	$$⊢\left(.\right]=\left(x\in {ℝ}^{*},y\in {ℝ}^{*}⟼\left\{z\in {ℝ}^{*}|\left(x<z\wedge z\le y\right)\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cioc	$$class\left(.\right]$$
1		vx	$$setvarx$$
2		cxr	$$class{ℝ}^{*}$$
3		vy	$$setvary$$
4		vz	$$setvarz$$
5	1	cv	$$setvarx$$
6		clt	$$class<$$
7	4	cv	$$setvarz$$
8	5 7 6	wbr	$$wffx<z$$
9		cle	$$class\le$$
10	3	cv	$$setvary$$
11	7 10 9	wbr	$$wffz\le y$$
12	8 11	wa	$$wff\left(x<z\wedge z\le y\right)$$
13	12 4 2	crab	$$class\left\{z\in {ℝ}^{*}|\left(x<z\wedge z\le y\right)\right\}$$
14	1 3 2 2 13	cmpo	$$class\left(x\in {ℝ}^{*},y\in {ℝ}^{*}⟼\left\{z\in {ℝ}^{*}|\left(x<z\wedge z\le y\right)\right\}\right)$$
15	0 14	wceq	$$wff\left(.\right]=\left(x\in {ℝ}^{*},y\in {ℝ}^{*}⟼\left\{z\in {ℝ}^{*}|\left(x<z\wedge z\le y\right)\right\}\right)$$