Definition df-icc 6364

Description: Define the set of closed intervals of extended reals.

Assertion

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

Distinct variable group:   x,y,z,w

Detailed syntax breakdown of Definition df-icc

Step	Hyp	Ref	Expression
1		cicc 6360	. 2 class [,]
2		vx	. . . . . . 7 set x
3	2	cv 955	. . . . . 6 class x
4		cxr 5485	. . . . . 6 class RR*
5	3, 4	wcel 958	. . . . 5 wff x e. RR*
6		vy	. . . . . . 7 set y
7	6	cv 955	. . . . . 6 class y
8	7, 4	wcel 958	. . . . 5 wff y e. RR*
9	5, 8	wa 223	. . . 4 wff (x e. RR* /\ y e. RR*)
10		vz	. . . . . 6 set z
11	10	cv 955	. . . . 5 class z
12		vw	. . . . . . . . 9 set w
13	12	cv 955	. . . . . . . 8 class w
14		cle 5295	. . . . . . . 8 class <_
15	3, 13, 14	wbr 2619	. . . . . . 7 wff x <_ w
16	13, 7, 14	wbr 2619	. . . . . . 7 wff w <_ y
17	15, 16	wa 223	. . . . . 6 wff (x <_ w /\ w <_ y)
18	17, 12, 4	crab 1648	. . . . 5 class {w e. RR* | (x <_ w /\ w <_ y)}
19	11, 18	wceq 956	. . . 4 wff z = {w e. RR* | (x <_ w /\ w <_ y)}
20	9, 19	wa 223	. . 3 wff ((x e. RR* /\ y e. RR*) /\ z = {w e. RR* | (x <_ w /\ w <_ y)})
21	20, 2, 6, 10	copab2 3964	. 2 class {<.<.x, y>., z>. | ((x e. RR* /\ y e. RR*) /\ z = {w e. RR* | (x <_ w /\ w <_ y)})}
22	1, 21	wceq 956	1 wff [,] = {<.<.x, y>., z>. | ((x e. RR* /\ y e. RR*) /\ z = {w e. RR* | (x <_ w /\ w <_ y)})}

This definition is referenced by:  iccvalt 6377  iccf 6401

Copyright terms: Public domain