Definition df-ioo 13092

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 13088	. 2 class (,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11017	. . 3 class ℝ*
5	2	cv 1538	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1538	. . . . . 6 class 𝑧
8		clt 11018	. . . . . 6 class <
9	5, 7, 8	wbr 5075	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1538	. . . . . 6 class 𝑦
11	7, 10, 8	wbr 5075	. . . . 5 wff 𝑧 < 𝑦
12	9, 11	wa 396	. . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)
13	12, 6, 4	crab 3069	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}
14	2, 3, 4, 4, 13	cmpo 7286	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
15	1, 14	wceq 1539	1 wff (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})

This definition is referenced by:  iooex  13111  iooval  13112  ndmioo  13115  elioo3g  13117  iooin  13122  iooss1  13123  iooss2  13124  elioo1  13128  iccssioo  13157  ioossicc  13174  ioossico  13179  iocssioo  13180  icossioo  13181  ioossioo  13182  ioof  13188  ioounsn  13218  snunioo  13219  ioodisj  13223  ioojoin  13224  ioopnfsup  13593  leordtval  22373  icopnfcld  23940  iocmnfcld  23941  bndth  24130  ioombl  24738  ioorf  24746  ioorinv2  24748  ismbf3d  24827  dvfsumrlimge0  25203  dvfsumrlim2  25205  tanord1  25702  dvloglem  25812  rlimcnp  26124  rlimcnp2  26125  dchrisum0lem2a  26674  pnt  26771  joiniooico  31104  tpr2rico  31871  asindmre  35869  dvasin  35870  ioossioc  43037  snunioo1  43057  ioossioobi  43062