Definition df-ioo 13450

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

This definition is used by:  iooex  13469  iooval  13470  ndmioo  13473  elioo3g  13475  iooin  13480  iooss1  13481  iooss2  13482  elioo1  13486  iccssioo  13516  ioossicc  13534  ioossico  13539  iocssioo  13540  icossioo  13541  ioossioo  13542  ioof  13548  ioounsn  13578  snunioo  13579  ioodisj  13583  ioojoin  13584  ioopnfsup  13973  leordtval  23493  icopnfcld  25048  iocmnfcld  25049  bndth  25241  ioombl  25848  ioorf  25856  ioorinv2  25858  ismbf3d  25937  dvfsumrlimge0  26312  dvfsumrlim2  26314  tanord1  26829  dvloglem  26940  rlimcnp  27257  rlimcnp2  27258  dchrisum0lem2a  27808  pnt  27905  joiniooico  33300  tpr2rico  34478  asindmre  38541  dvasin  38542  iocioodisjd  43299  ioossioc  46426  snunioo1  46446  ioossioobi  46451