Definition df-ioo 12818

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 12814	. 2 class (,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 10745	. . 3 class ℝ*
5	2	cv 1541	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1541	. . . . . 6 class 𝑧
8		clt 10746	. . . . . 6 class <
9	5, 7, 8	wbr 5027	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1541	. . . . . 6 class 𝑦
11	7, 10, 8	wbr 5027	. . . . 5 wff 𝑧 < 𝑦
12	9, 11	wa 399	. . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)
13	12, 6, 4	crab 3057	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}
14	2, 3, 4, 4, 13	cmpo 7166	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
15	1, 14	wceq 1542	1 wff (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})

This definition is referenced by:  iooex  12837  iooval  12838  ndmioo  12841  elioo3g  12843  iooin  12848  iooss1  12849  iooss2  12850  elioo1  12854  iccssioo  12883  ioossicc  12900  ioossico  12905  iocssioo  12906  icossioo  12907  ioossioo  12908  ioof  12914  ioounsn  12944  snunioo  12945  ioodisj  12949  ioojoin  12950  ioopnfsup  13316  leordtval  21957  icopnfcld  23513  iocmnfcld  23514  bndth  23703  ioombl  24310  ioorf  24318  ioorinv2  24320  ismbf3d  24399  dvfsumrlimge0  24774  dvfsumrlim2  24776  tanord1  25273  dvloglem  25383  rlimcnp  25695  rlimcnp2  25696  dchrisum0lem2a  26245  pnt  26342  joiniooico  30662  tpr2rico  31426  asindmre  35472  dvasin  35473  ioossioc  42554  snunioo1  42574  ioossioobi  42579