Definition df-ioo 13507

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 13503	. 2 class (,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11369	. . 3 class ℝ*
5	2	cv 1569	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1569	. . . . . 6 class 𝑧
8		clt 11370	. . . . . 6 class <
9	5, 7, 8	wbr 5106	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1569	. . . . . 6 class 𝑦
11	7, 10, 8	wbr 5106	. . . . 5 wff 𝑧 < 𝑦
12	9, 11	wa 401	. . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)
13	12, 6, 4	crab 3416	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}
14	2, 3, 4, 4, 13	cmpo 7445	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
15	1, 14	wceq 1570	1 wff (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})

This definition is used by:  iooex  13526  iooval  13527  ndmioo  13530  elioo3g  13532  iooin  13537  iooss1  13538  iooss2  13539  elioo1  13543  iccssioo  13573  ioossicc  13591  ioossico  13596  iocssioo  13597  icossioo  13598  ioossioo  13599  ioof  13605  ioounsn  13635  snunioo  13636  ioodisj  13640  ioojoin  13641  ioopnfsup  14031  leordtval  23561  icopnfcld  25116  iocmnfcld  25117  bndth  25309  ioombl  25916  ioorf  25924  ioorinv2  25926  ismbf3d  26005  dvfsumrlimge0  26380  dvfsumrlim2  26382  tanord1  26895  dvloglem  27006  rlimcnp  27323  rlimcnp2  27324  dchrisum0lem2a  27874  pnt  27971  joiniooico  33436  tpr2rico  34614  asindmre  38813  dvasin  38814  iocioodisjd  43570  ioossioc  46709  snunioo1  46729  ioossioobi  46734