Definition df-ioo 13386

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

This definition is used by:  iooex  13405  iooval  13406  ndmioo  13409  elioo3g  13411  iooin  13416  iooss1  13417  iooss2  13418  elioo1  13422  iccssioo  13452  ioossicc  13470  ioossico  13475  iocssioo  13476  icossioo  13477  ioossioo  13478  ioof  13484  ioounsn  13514  snunioo  13515  ioodisj  13519  ioojoin  13520  ioopnfsup  13908  leordtval  23385  icopnfcld  24939  iocmnfcld  24940  bndth  25132  ioombl  25739  ioorf  25747  ioorinv2  25749  ismbf3d  25828  dvfsumrlimge0  26204  dvfsumrlim2  26206  tanord1  26717  dvloglem  26828  rlimcnp  27145  rlimcnp2  27146  dchrisum0lem2a  27696  pnt  27793  joiniooico  33134  tpr2rico  34315  asindmre  38386  dvasin  38387  iocioodisjd  43113  ioossioc  46240  snunioo1  46260  ioossioobi  46265