Definition df-ioo 12743

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 12739	. 2 class (,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 10674	. . 3 class ℝ*
5	2	cv 1536	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1536	. . . . . 6 class 𝑧
8		clt 10675	. . . . . 6 class <
9	5, 7, 8	wbr 5066	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1536	. . . . . 6 class 𝑦
11	7, 10, 8	wbr 5066	. . . . 5 wff 𝑧 < 𝑦
12	9, 11	wa 398	. . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)
13	12, 6, 4	crab 3142	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}
14	2, 3, 4, 4, 13	cmpo 7158	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
15	1, 14	wceq 1537	1 wff (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})

This definition is referenced by:  iooex  12762  iooval  12763  ndmioo  12766  elioo3g  12768  iooin  12773  iooss1  12774  iooss2  12775  elioo1  12779  iccssioo  12806  ioossicc  12823  ioossico  12827  iocssioo  12828  icossioo  12829  ioossioo  12830  ioof  12836  ioounsn  12864  snunioo  12865  ioodisj  12869  ioojoin  12870  ioopnfsup  13233  leordtval  21821  icopnfcld  23376  iocmnfcld  23377  bndth  23562  ioombl  24166  ioorf  24174  ioorinv2  24176  ismbf3d  24255  dvfsumrlimge0  24627  dvfsumrlim2  24629  tanord1  25121  dvloglem  25231  rlimcnp  25543  rlimcnp2  25544  dchrisum0lem2a  26093  pnt  26190  joiniooico  30497  tpr2rico  31155  asindmre  34992  dvasin  34993  ioossioc  41815  snunioo1  41837  ioossioobi  41842