Definition df-ioc 13359

Description: Define the set of open-below, closed-above intervals of extended reals. (Contributed by NM, 24-Dec-2006.)

Assertion

Ref	Expression
df-ioc	⊢ (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})

Distinct variable group:   𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-ioc

Step	Hyp	Ref	Expression
1		cioc 13355	. 2 class (,]
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11261	. . 3 class ℝ*
5	2	cv 1538	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1538	. . . . . 6 class 𝑧
8		clt 11262	. . . . . 6 class <
9	5, 7, 8	wbr 5117	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1538	. . . . . 6 class 𝑦
11		cle 11263	. . . . . 6 class ≤
12	7, 10, 11	wbr 5117	. . . . 5 wff 𝑧 ≤ 𝑦
13	9, 12	wa 395	. . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)
14	13, 6, 4	crab 3413	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}
15	2, 3, 4, 4, 14	cmpo 7402	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})
16	1, 15	wceq 1539	1 wff (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})

This definition is referenced by:  iocval  13391  elioc1  13396  iocssxr  13438  iocssicc  13444  iocssioo  13446  ioounsn  13484  snunioc  13487  leordtval2  23137  iocpnfordt  23140  lecldbas  23144  pnfnei  23145  iocmnfcld  24694  xrtgioo  24733  ismbf3d  25594  dvloglem  26595  asindmre  37656  dvasin  37657  iocioodisjd  42300  ioossioc  45455  eliocre  45472  lbioc  45476