Definition df-ioo 13367

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 13363	. 2 class (,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11230	. . 3 class ℝ*
5	2	cv 1562	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1562	. . . . . 6 class 𝑧
8		clt 11231	. . . . . 6 class <
9	5, 7, 8	wbr 5105	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1562	. . . . . 6 class 𝑦
11	7, 10, 8	wbr 5105	. . . . 5 wff 𝑧 < 𝑦
12	9, 11	wa 400	. . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)
13	12, 6, 4	crab 3417	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}
14	2, 3, 4, 4, 13	cmpo 7402	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
15	1, 14	wceq 1563	1 wff (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})

This definition is referenced by:  iooex  13386  iooval  13387  ndmioo  13390  elioo3g  13392  iooin  13397  iooss1  13398  iooss2  13399  elioo1  13403  iccssioo  13433  ioossicc  13451  ioossico  13456  iocssioo  13457  icossioo  13458  ioossioo  13459  ioof  13465  ioounsn  13495  snunioo  13496  ioodisj  13500  ioojoin  13501  ioopnfsup  13888  leordtval  23331  icopnfcld  24885  iocmnfcld  24886  bndth  25078  ioombl  25685  ioorf  25693  ioorinv2  25695  ismbf3d  25774  dvfsumrlimge0  26150  dvfsumrlim2  26152  tanord1  26660  dvloglem  26771  rlimcnp  27088  rlimcnp2  27089  dchrisum0lem2a  27639  pnt  27736  joiniooico  33031  tpr2rico  34219  asindmre  38214  dvasin  38215  iocioodisjd  42941  ioossioc  46066  snunioo1  46086  ioossioobi  46091