Definition df-ioo 12467

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 12463	. 2 class (,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 10390	. . 3 class ℝ*
5	2	cv 1655	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1655	. . . . . 6 class 𝑧
8		clt 10391	. . . . . 6 class <
9	5, 7, 8	wbr 4873	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1655	. . . . . 6 class 𝑦
11	7, 10, 8	wbr 4873	. . . . 5 wff 𝑧 < 𝑦
12	9, 11	wa 386	. . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)
13	12, 6, 4	crab 3121	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}
14	2, 3, 4, 4, 13	cmpt2 6907	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
15	1, 14	wceq 1656	1 wff (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})

This definition is referenced by:  iooex  12486  iooval  12487  ndmioo  12490  elioo3g  12492  iooin  12497  iooss1  12498  iooss2  12499  elioo1  12503  iccssioo  12530  ioossicc  12547  ioossico  12551  iocssioo  12552  icossioo  12553  ioossioo  12554  ioof  12560  ioounsn  12589  ioounsnOLD  12590  snunioo  12591  ioodisj  12595  ioojoin  12596  ioopnfsup  12958  leordtval  21388  icopnfcld  22941  iocmnfcld  22942  bndth  23127  ioombl  23731  ioorf  23739  ioorinv2  23741  ismbf3d  23820  dvfsumrlimge0  24192  dvfsumrlim2  24194  tanord1  24683  dvloglem  24793  rlimcnp  25105  rlimcnp2  25106  dchrisum0lem2a  25619  pnt  25716  joiniooico  30072  tpr2rico  30492  asindmre  34031  dvasin  34032  ioossioc  40505  snunioo1  40527  ioossioobi  40532