Definition df-ioo 13391

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 13387	. 2 class (,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11294	. . 3 class ℝ*
5	2	cv 1539	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1539	. . . . . 6 class 𝑧
8		clt 11295	. . . . . 6 class <
9	5, 7, 8	wbr 5143	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1539	. . . . . 6 class 𝑦
11	7, 10, 8	wbr 5143	. . . . 5 wff 𝑧 < 𝑦
12	9, 11	wa 395	. . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)
13	12, 6, 4	crab 3436	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}
14	2, 3, 4, 4, 13	cmpo 7433	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
15	1, 14	wceq 1540	1 wff (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})

This definition is referenced by:  iooex  13410  iooval  13411  ndmioo  13414  elioo3g  13416  iooin  13421  iooss1  13422  iooss2  13423  elioo1  13427  iccssioo  13456  ioossicc  13473  ioossico  13478  iocssioo  13479  icossioo  13480  ioossioo  13481  ioof  13487  ioounsn  13517  snunioo  13518  ioodisj  13522  ioojoin  13523  ioopnfsup  13904  leordtval  23221  icopnfcld  24788  iocmnfcld  24789  bndth  24990  ioombl  25600  ioorf  25608  ioorinv2  25610  ismbf3d  25689  dvfsumrlimge0  26071  dvfsumrlim2  26073  tanord1  26579  dvloglem  26690  rlimcnp  27008  rlimcnp2  27009  dchrisum0lem2a  27561  pnt  27658  joiniooico  32776  tpr2rico  33911  asindmre  37710  dvasin  37711  iocioodisjd  42355  ioossioc  45505  snunioo1  45525  ioossioobi  45530