Definition df-ioo 13012

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 13008	. 2 class (,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 10939	. . 3 class ℝ*
5	2	cv 1538	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1538	. . . . . 6 class 𝑧
8		clt 10940	. . . . . 6 class <
9	5, 7, 8	wbr 5070	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1538	. . . . . 6 class 𝑦
11	7, 10, 8	wbr 5070	. . . . 5 wff 𝑧 < 𝑦
12	9, 11	wa 395	. . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)
13	12, 6, 4	crab 3067	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}
14	2, 3, 4, 4, 13	cmpo 7257	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
15	1, 14	wceq 1539	1 wff (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})

This definition is referenced by:  iooex  13031  iooval  13032  ndmioo  13035  elioo3g  13037  iooin  13042  iooss1  13043  iooss2  13044  elioo1  13048  iccssioo  13077  ioossicc  13094  ioossico  13099  iocssioo  13100  icossioo  13101  ioossioo  13102  ioof  13108  ioounsn  13138  snunioo  13139  ioodisj  13143  ioojoin  13144  ioopnfsup  13512  leordtval  22272  icopnfcld  23837  iocmnfcld  23838  bndth  24027  ioombl  24634  ioorf  24642  ioorinv2  24644  ismbf3d  24723  dvfsumrlimge0  25099  dvfsumrlim2  25101  tanord1  25598  dvloglem  25708  rlimcnp  26020  rlimcnp2  26021  dchrisum0lem2a  26570  pnt  26667  joiniooico  30997  tpr2rico  31764  asindmre  35787  dvasin  35788  ioossioc  42920  snunioo1  42940  ioossioobi  42945