Definition df-ioo 13332

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 13328	. 2 class (,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11251	. . 3 class ℝ*
5	2	cv 1540	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1540	. . . . . 6 class 𝑧
8		clt 11252	. . . . . 6 class <
9	5, 7, 8	wbr 5148	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1540	. . . . . 6 class 𝑦
11	7, 10, 8	wbr 5148	. . . . 5 wff 𝑧 < 𝑦
12	9, 11	wa 396	. . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)
13	12, 6, 4	crab 3432	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}
14	2, 3, 4, 4, 13	cmpo 7413	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
15	1, 14	wceq 1541	1 wff (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})

This definition is referenced by:  iooex  13351  iooval  13352  ndmioo  13355  elioo3g  13357  iooin  13362  iooss1  13363  iooss2  13364  elioo1  13368  iccssioo  13397  ioossicc  13414  ioossico  13419  iocssioo  13420  icossioo  13421  ioossioo  13422  ioof  13428  ioounsn  13458  snunioo  13459  ioodisj  13463  ioojoin  13464  ioopnfsup  13833  leordtval  22937  icopnfcld  24504  iocmnfcld  24505  bndth  24698  ioombl  25306  ioorf  25314  ioorinv2  25316  ismbf3d  25395  dvfsumrlimge0  25771  dvfsumrlim2  25773  tanord1  26270  dvloglem  26380  rlimcnp  26694  rlimcnp2  26695  dchrisum0lem2a  27244  pnt  27341  joiniooico  32240  tpr2rico  33178  asindmre  36874  dvasin  36875  ioossioc  44504  snunioo1  44524  ioossioobi  44529