Definition df-ioo 13323

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 13319	. 2 class (,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11242	. . 3 class ℝ*
5	2	cv 1541	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1541	. . . . . 6 class 𝑧
8		clt 11243	. . . . . 6 class <
9	5, 7, 8	wbr 5146	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1541	. . . . . 6 class 𝑦
11	7, 10, 8	wbr 5146	. . . . 5 wff 𝑧 < 𝑦
12	9, 11	wa 397	. . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)
13	12, 6, 4	crab 3433	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}
14	2, 3, 4, 4, 13	cmpo 7405	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
15	1, 14	wceq 1542	1 wff (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})

This definition is referenced by:  iooex  13342  iooval  13343  ndmioo  13346  elioo3g  13348  iooin  13353  iooss1  13354  iooss2  13355  elioo1  13359  iccssioo  13388  ioossicc  13405  ioossico  13410  iocssioo  13411  icossioo  13412  ioossioo  13413  ioof  13419  ioounsn  13449  snunioo  13450  ioodisj  13454  ioojoin  13455  ioopnfsup  13824  leordtval  22698  icopnfcld  24265  iocmnfcld  24266  bndth  24455  ioombl  25063  ioorf  25071  ioorinv2  25073  ismbf3d  25152  dvfsumrlimge0  25528  dvfsumrlim2  25530  tanord1  26027  dvloglem  26137  rlimcnp  26449  rlimcnp2  26450  dchrisum0lem2a  26999  pnt  27096  joiniooico  31962  tpr2rico  32829  asindmre  36508  dvasin  36509  ioossioc  44139  snunioo1  44159  ioossioobi  44164