Definition df-ioo 13325

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 13321	. 2 class (,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11244	. . 3 class ℝ*
5	2	cv 1541	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1541	. . . . . 6 class 𝑧
8		clt 11245	. . . . . 6 class <
9	5, 7, 8	wbr 5148	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1541	. . . . . 6 class 𝑦
11	7, 10, 8	wbr 5148	. . . . 5 wff 𝑧 < 𝑦
12	9, 11	wa 397	. . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)
13	12, 6, 4	crab 3433	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}
14	2, 3, 4, 4, 13	cmpo 7408	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
15	1, 14	wceq 1542	1 wff (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})

This definition is referenced by:  iooex  13344  iooval  13345  ndmioo  13348  elioo3g  13350  iooin  13355  iooss1  13356  iooss2  13357  elioo1  13361  iccssioo  13390  ioossicc  13407  ioossico  13412  iocssioo  13413  icossioo  13414  ioossioo  13415  ioof  13421  ioounsn  13451  snunioo  13452  ioodisj  13456  ioojoin  13457  ioopnfsup  13826  leordtval  22709  icopnfcld  24276  iocmnfcld  24277  bndth  24466  ioombl  25074  ioorf  25082  ioorinv2  25084  ismbf3d  25163  dvfsumrlimge0  25539  dvfsumrlim2  25541  tanord1  26038  dvloglem  26148  rlimcnp  26460  rlimcnp2  26461  dchrisum0lem2a  27010  pnt  27107  joiniooico  31973  tpr2rico  32881  asindmre  36560  dvasin  36561  ioossioc  44192  snunioo1  44212  ioossioobi  44217