Definition df-ioo 13270

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

Assertion

Ref	Expression
df-ioo	⊢ (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})

Distinct variable group:   𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-ioo

Step	Hyp	Ref	Expression
1		cioo 13266	. 2 class (,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11170	. . 3 class ℝ*
5	2	cv 1541	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1541	. . . . . 6 class 𝑧
8		clt 11171	. . . . . 6 class <
9	5, 7, 8	wbr 5099	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1541	. . . . . 6 class 𝑦
11	7, 10, 8	wbr 5099	. . . . 5 wff 𝑧 < 𝑦
12	9, 11	wa 395	. . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)
13	12, 6, 4	crab 3400	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}
14	2, 3, 4, 4, 13	cmpo 7363	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
15	1, 14	wceq 1542	1 wff (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})

This definition is referenced by:  iooex  13289  iooval  13290  ndmioo  13293  elioo3g  13295  iooin  13300  iooss1  13301  iooss2  13302  elioo1  13306  iccssioo  13336  ioossicc  13354  ioossico  13359  iocssioo  13360  icossioo  13361  ioossioo  13362  ioof  13368  ioounsn  13398  snunioo  13399  ioodisj  13403  ioojoin  13404  ioopnfsup  13789  leordtval  23162  icopnfcld  24716  iocmnfcld  24717  bndth  24918  ioombl  25527  ioorf  25535  ioorinv2  25537  ismbf3d  25616  dvfsumrlimge0  25998  dvfsumrlim2  26000  tanord1  26507  dvloglem  26618  rlimcnp  26936  rlimcnp2  26937  dchrisum0lem2a  27489  pnt  27586  joiniooico  32857  tpr2rico  34082  asindmre  37917  dvasin  37918  iocioodisjd  42653  ioossioc  45815  snunioo1  45835  ioossioobi  45840