Definition df-ioo

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cioo	$$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	3	cv	$$setvary$$
10	7 9 6	wbr	$$wffz<y$$
11	8 10	wa	$$wff\left(x<z\wedge z<y\right)$$
12	11 4 2	crab	$$class\left\{z\in {ℝ}^{*}|\left(x<z\wedge z<y\right)\right\}$$
13	1 3 2 2 12	cmpo	$$class\left(x\in {ℝ}^{*},y\in {ℝ}^{*}⟼\left\{z\in {ℝ}^{*}|\left(x<z\wedge z<y\right)\right\}\right)$$
14	0 13	wceq	$$wff\left(.\right)=\left(x\in {ℝ}^{*},y\in {ℝ}^{*}⟼\left\{z\in {ℝ}^{*}|\left(x<z\wedge z<y\right)\right\}\right)$$