Definition df-ioo 13481

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 13477	. 2 class (,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11343	. . 3 class ℝ*
5	2	cv 1568	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1568	. . . . . 6 class 𝑧
8		clt 11344	. . . . . 6 class <
9	5, 7, 8	wbr 5102	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1568	. . . . . 6 class 𝑦
11	7, 10, 8	wbr 5102	. . . . 5 wff 𝑧 < 𝑦
12	9, 11	wa 401	. . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)
13	12, 6, 4	crab 3412	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}
14	2, 3, 4, 4, 13	cmpo 7422	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
15	1, 14	wceq 1569	1 wff (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})

This definition is used by:  iooex  13500  iooval  13501  ndmioo  13504  elioo3g  13506  iooin  13511  iooss1  13512  iooss2  13513  elioo1  13517  iccssioo  13547  ioossicc  13565  ioossico  13570  iocssioo  13571  icossioo  13572  ioossioo  13573  ioof  13579  ioounsn  13609  snunioo  13610  ioodisj  13614  ioojoin  13615  ioopnfsup  14005  leordtval  23532  icopnfcld  25087  iocmnfcld  25088  bndth  25280  ioombl  25887  ioorf  25895  ioorinv2  25897  ismbf3d  25976  dvfsumrlimge0  26351  dvfsumrlim2  26353  tanord1  26866  dvloglem  26977  rlimcnp  27294  rlimcnp2  27295  dchrisum0lem2a  27845  pnt  27942  joiniooico  33409  tpr2rico  34587  asindmre  38697  dvasin  38698  iocioodisjd  43453  ioossioc  46580  snunioo1  46600  ioossioobi  46605