Definition df-icc

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

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

Detailed syntax breakdown

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