Definition df-ioo 13411

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 13407	. 2 class (,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11323	. . 3 class ℝ*
5	2	cv 1536	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1536	. . . . . 6 class 𝑧
8		clt 11324	. . . . . 6 class <
9	5, 7, 8	wbr 5166	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1536	. . . . . 6 class 𝑦
11	7, 10, 8	wbr 5166	. . . . 5 wff 𝑧 < 𝑦
12	9, 11	wa 395	. . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)
13	12, 6, 4	crab 3443	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}
14	2, 3, 4, 4, 13	cmpo 7450	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
15	1, 14	wceq 1537	1 wff (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})

This definition is referenced by:  iooex  13430  iooval  13431  ndmioo  13434  elioo3g  13436  iooin  13441  iooss1  13442  iooss2  13443  elioo1  13447  iccssioo  13476  ioossicc  13493  ioossico  13498  iocssioo  13499  icossioo  13500  ioossioo  13501  ioof  13507  ioounsn  13537  snunioo  13538  ioodisj  13542  ioojoin  13543  ioopnfsup  13915  leordtval  23242  icopnfcld  24809  iocmnfcld  24810  bndth  25009  ioombl  25619  ioorf  25627  ioorinv2  25629  ismbf3d  25708  dvfsumrlimge0  26091  dvfsumrlim2  26093  tanord1  26597  dvloglem  26708  rlimcnp  27026  rlimcnp2  27027  dchrisum0lem2a  27579  pnt  27676  joiniooico  32779  tpr2rico  33858  asindmre  37663  dvasin  37664  ioossioc  45410  snunioo1  45430  ioossioobi  45435