Definition df-ioo 13387

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 13383	. 2 class (,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11291	. . 3 class ℝ*
5	2	cv 1535	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1535	. . . . . 6 class 𝑧
8		clt 11292	. . . . . 6 class <
9	5, 7, 8	wbr 5147	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1535	. . . . . 6 class 𝑦
11	7, 10, 8	wbr 5147	. . . . 5 wff 𝑧 < 𝑦
12	9, 11	wa 395	. . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)
13	12, 6, 4	crab 3432	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}
14	2, 3, 4, 4, 13	cmpo 7432	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
15	1, 14	wceq 1536	1 wff (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})

This definition is referenced by:  iooex  13406  iooval  13407  ndmioo  13410  elioo3g  13412  iooin  13417  iooss1  13418  iooss2  13419  elioo1  13423  iccssioo  13452  ioossicc  13469  ioossico  13474  iocssioo  13475  icossioo  13476  ioossioo  13477  ioof  13483  ioounsn  13513  snunioo  13514  ioodisj  13518  ioojoin  13519  ioopnfsup  13900  leordtval  23236  icopnfcld  24803  iocmnfcld  24804  bndth  25003  ioombl  25613  ioorf  25621  ioorinv2  25623  ismbf3d  25702  dvfsumrlimge0  26085  dvfsumrlim2  26087  tanord1  26593  dvloglem  26704  rlimcnp  27022  rlimcnp2  27023  dchrisum0lem2a  27575  pnt  27672  joiniooico  32782  tpr2rico  33872  asindmre  37689  dvasin  37690  iocioodisjd  42333  ioossioc  45444  snunioo1  45464  ioossioobi  45469