Definition df-ico

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

	Ref	Expression
Assertion	df-ico	$$⊢\left[.\right)=\left(x\in {ℝ}^{*},y\in {ℝ}^{*}⟼\left\{z\in {ℝ}^{*}|\left(x\le z\wedge z<y\right)\right\}\right)$$

Detailed syntax breakdown

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