Definition df-ioo 13270

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

This definition is referenced by:  iooex  13289  iooval  13290  ndmioo  13293  elioo3g  13295  iooin  13300  iooss1  13301  iooss2  13302  elioo1  13306  iccssioo  13336  ioossicc  13354  ioossico  13359  iocssioo  13360  icossioo  13361  ioossioo  13362  ioof  13368  ioounsn  13398  snunioo  13399  ioodisj  13403  ioojoin  13404  ioopnfsup  13786  leordtval  23116  icopnfcld  24671  iocmnfcld  24672  bndth  24873  ioombl  25482  ioorf  25490  ioorinv2  25492  ismbf3d  25571  dvfsumrlimge0  25953  dvfsumrlim2  25955  tanord1  26462  dvloglem  26573  rlimcnp  26891  rlimcnp2  26892  dchrisum0lem2a  27444  pnt  27541  joiniooico  32730  tpr2rico  33878  asindmre  37682  dvasin  37683  iocioodisjd  42293  ioossioc  45474  snunioo1  45494  ioossioobi  45499