Definition df-ioo 6361

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

Assertion

Ref	Expression
df-ioo	|- (,) = {<.<.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-ioo

Step	Hyp	Ref	Expression
1		cioo 6357	. 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		clt 5486	. . . . . . . 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:  iooex 6365  ioovalt 6366  ndmioo 6370  elioo3g 6380  ioof 6400  bsi 10495

Copyright terms: Public domain