Definition df-ioo 13302

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 13298	. 2 class (,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11178	. . 3 class ℝ*
5	2	cv 1541	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1541	. . . . . 6 class 𝑧
8		clt 11179	. . . . . 6 class <
9	5, 7, 8	wbr 5086	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1541	. . . . . 6 class 𝑦
11	7, 10, 8	wbr 5086	. . . . 5 wff 𝑧 < 𝑦
12	9, 11	wa 395	. . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)
13	12, 6, 4	crab 3390	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}
14	2, 3, 4, 4, 13	cmpo 7369	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
15	1, 14	wceq 1542	1 wff (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})

This definition is referenced by:  iooex  13321  iooval  13322  ndmioo  13325  elioo3g  13327  iooin  13332  iooss1  13333  iooss2  13334  elioo1  13338  iccssioo  13368  ioossicc  13386  ioossico  13391  iocssioo  13392  icossioo  13393  ioossioo  13394  ioof  13400  ioounsn  13430  snunioo  13431  ioodisj  13435  ioojoin  13436  ioopnfsup  13823  leordtval  23178  icopnfcld  24732  iocmnfcld  24733  bndth  24925  ioombl  25532  ioorf  25540  ioorinv2  25542  ismbf3d  25621  dvfsumrlimge0  25997  dvfsumrlim2  25999  tanord1  26501  dvloglem  26612  rlimcnp  26929  rlimcnp2  26930  dchrisum0lem2a  27480  pnt  27577  joiniooico  32847  tpr2rico  34056  asindmre  38024  dvasin  38025  iocioodisjd  42752  ioossioc  45922  snunioo1  45942  ioossioobi  45947