Definition df-ioo 13293

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 13289	. 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 5086	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1541	. . . . . 6 class 𝑦
11	7, 10, 8	wbr 5086	. . . . 5 wff 𝑧 < 𝑦
12	9, 11	wa 395	. . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)
13	12, 6, 4	crab 3390	. . 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  13312  iooval  13313  ndmioo  13316  elioo3g  13318  iooin  13323  iooss1  13324  iooss2  13325  elioo1  13329  iccssioo  13359  ioossicc  13377  ioossico  13382  iocssioo  13383  icossioo  13384  ioossioo  13385  ioof  13391  ioounsn  13421  snunioo  13422  ioodisj  13426  ioojoin  13427  ioopnfsup  13814  leordtval  23188  icopnfcld  24742  iocmnfcld  24743  bndth  24935  ioombl  25542  ioorf  25550  ioorinv2  25552  ismbf3d  25631  dvfsumrlimge0  26007  dvfsumrlim2  26009  tanord1  26514  dvloglem  26625  rlimcnp  26942  rlimcnp2  26943  dchrisum0lem2a  27494  pnt  27591  joiniooico  32862  tpr2rico  34072  asindmre  38038  dvasin  38039  iocioodisjd  42766  ioossioc  45940  snunioo1  45960  ioossioobi  45965