Definition df-ioo 13241

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 13237	. 2 class (,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11137	. . 3 class ℝ*
5	2	cv 1540	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1540	. . . . . 6 class 𝑧
8		clt 11138	. . . . . 6 class <
9	5, 7, 8	wbr 5089	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1540	. . . . . 6 class 𝑦
11	7, 10, 8	wbr 5089	. . . . 5 wff 𝑧 < 𝑦
12	9, 11	wa 395	. . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)
13	12, 6, 4	crab 3393	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}
14	2, 3, 4, 4, 13	cmpo 7343	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
15	1, 14	wceq 1541	1 wff (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})

This definition is referenced by:  iooex  13260  iooval  13261  ndmioo  13264  elioo3g  13266  iooin  13271  iooss1  13272  iooss2  13273  elioo1  13277  iccssioo  13307  ioossicc  13325  ioossico  13330  iocssioo  13331  icossioo  13332  ioossioo  13333  ioof  13339  ioounsn  13369  snunioo  13370  ioodisj  13374  ioojoin  13375  ioopnfsup  13760  leordtval  23121  icopnfcld  24675  iocmnfcld  24676  bndth  24877  ioombl  25486  ioorf  25494  ioorinv2  25496  ismbf3d  25575  dvfsumrlimge0  25957  dvfsumrlim2  25959  tanord1  26466  dvloglem  26577  rlimcnp  26895  rlimcnp2  26896  dchrisum0lem2a  27448  pnt  27545  joiniooico  32747  tpr2rico  33915  asindmre  37722  dvasin  37723  iocioodisjd  42332  ioossioc  45511  snunioo1  45531  ioossioobi  45536