Definition df-ioo 13310

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 13306	. 2 class (,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11207	. . 3 class ℝ*
5	2	cv 1539	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1539	. . . . . 6 class 𝑧
8		clt 11208	. . . . . 6 class <
9	5, 7, 8	wbr 5107	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1539	. . . . . 6 class 𝑦
11	7, 10, 8	wbr 5107	. . . . 5 wff 𝑧 < 𝑦
12	9, 11	wa 395	. . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)
13	12, 6, 4	crab 3405	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}
14	2, 3, 4, 4, 13	cmpo 7389	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
15	1, 14	wceq 1540	1 wff (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})

This definition is referenced by:  iooex  13329  iooval  13330  ndmioo  13333  elioo3g  13335  iooin  13340  iooss1  13341  iooss2  13342  elioo1  13346  iccssioo  13376  ioossicc  13394  ioossico  13399  iocssioo  13400  icossioo  13401  ioossioo  13402  ioof  13408  ioounsn  13438  snunioo  13439  ioodisj  13443  ioojoin  13444  ioopnfsup  13826  leordtval  23100  icopnfcld  24655  iocmnfcld  24656  bndth  24857  ioombl  25466  ioorf  25474  ioorinv2  25476  ismbf3d  25555  dvfsumrlimge0  25937  dvfsumrlim2  25939  tanord1  26446  dvloglem  26557  rlimcnp  26875  rlimcnp2  26876  dchrisum0lem2a  27428  pnt  27525  joiniooico  32697  tpr2rico  33902  asindmre  37697  dvasin  37698  iocioodisjd  42308  ioossioc  45490  snunioo1  45510  ioossioobi  45515