Definition df-ioo 13406

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 13402	. 2 class (,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11270	. . 3 class ℝ*
5	2	cv 1569	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1569	. . . . . 6 class 𝑧
8		clt 11271	. . . . . 6 class <
9	5, 7, 8	wbr 5107	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1569	. . . . . 6 class 𝑦
11	7, 10, 8	wbr 5107	. . . . 5 wff 𝑧 < 𝑦
12	9, 11	wa 401	. . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)
13	12, 6, 4	crab 3414	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}
14	2, 3, 4, 4, 13	cmpo 7419	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
15	1, 14	wceq 1570	1 wff (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})

This definition is used by:  iooex  13425  iooval  13426  ndmioo  13429  elioo3g  13431  iooin  13436  iooss1  13437  iooss2  13438  elioo1  13442  iccssioo  13472  ioossicc  13490  ioossico  13495  iocssioo  13496  icossioo  13497  ioossioo  13498  ioof  13504  ioounsn  13534  snunioo  13535  ioodisj  13539  ioojoin  13540  ioopnfsup  13929  leordtval  23444  icopnfcld  24999  iocmnfcld  25000  bndth  25192  ioombl  25799  ioorf  25807  ioorinv2  25809  ismbf3d  25888  dvfsumrlimge0  26264  dvfsumrlim2  26266  tanord1  26782  dvloglem  26893  rlimcnp  27210  rlimcnp2  27211  dchrisum0lem2a  27761  pnt  27858  joiniooico  33253  tpr2rico  34430  asindmre  38460  dvasin  38461  iocioodisjd  43203  ioossioc  46330  snunioo1  46350  ioossioobi  46355