Definition df-ioo 12730

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 12726	. 2 class (,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 10663	. . 3 class ℝ*
5	2	cv 1537	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1537	. . . . . 6 class 𝑧
8		clt 10664	. . . . . 6 class <
9	5, 7, 8	wbr 5030	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1537	. . . . . 6 class 𝑦
11	7, 10, 8	wbr 5030	. . . . 5 wff 𝑧 < 𝑦
12	9, 11	wa 399	. . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)
13	12, 6, 4	crab 3110	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}
14	2, 3, 4, 4, 13	cmpo 7137	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
15	1, 14	wceq 1538	1 wff (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})

This definition is referenced by:  iooex  12749  iooval  12750  ndmioo  12753  elioo3g  12755  iooin  12760  iooss1  12761  iooss2  12762  elioo1  12766  iccssioo  12794  ioossicc  12811  ioossico  12816  iocssioo  12817  icossioo  12818  ioossioo  12819  ioof  12825  ioounsn  12855  snunioo  12856  ioodisj  12860  ioojoin  12861  ioopnfsup  13227  leordtval  21818  icopnfcld  23373  iocmnfcld  23374  bndth  23563  ioombl  24169  ioorf  24177  ioorinv2  24179  ismbf3d  24258  dvfsumrlimge0  24633  dvfsumrlim2  24635  tanord1  25129  dvloglem  25239  rlimcnp  25551  rlimcnp2  25552  dchrisum0lem2a  26101  pnt  26198  joiniooico  30523  tpr2rico  31265  asindmre  35140  dvasin  35141  ioossioc  42129  snunioo1  42149  ioossioobi  42154