Definition df-ioo 13269

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 13265	. 2 class (,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11169	. . 3 class ℝ*
5	2	cv 1541	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1541	. . . . . 6 class 𝑧
8		clt 11170	. . . . . 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 7362	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
15	1, 14	wceq 1542	1 wff (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})

This definition is referenced by:  iooex  13288  iooval  13289  ndmioo  13292  elioo3g  13294  iooin  13299  iooss1  13300  iooss2  13301  elioo1  13305  iccssioo  13335  ioossicc  13353  ioossico  13358  iocssioo  13359  icossioo  13360  ioossioo  13361  ioof  13367  ioounsn  13397  snunioo  13398  ioodisj  13402  ioojoin  13403  ioopnfsup  13788  leordtval  23161  icopnfcld  24715  iocmnfcld  24716  bndth  24917  ioombl  25526  ioorf  25534  ioorinv2  25536  ismbf3d  25615  dvfsumrlimge0  25997  dvfsumrlim2  25999  tanord1  26506  dvloglem  26617  rlimcnp  26935  rlimcnp2  26936  dchrisum0lem2a  27488  pnt  27585  joiniooico  32835  tpr2rico  34050  asindmre  37875  dvasin  37876  iocioodisjd  42611  ioossioc  45774  snunioo1  45794  ioossioobi  45799