Definition df-ioc 13013

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 13009	. 2 class (,]
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 10939	. . 3 class ℝ*
5	2	cv 1538	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1538	. . . . . 6 class 𝑧
8		clt 10940	. . . . . 6 class <
9	5, 7, 8	wbr 5070	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1538	. . . . . 6 class 𝑦
11		cle 10941	. . . . . 6 class ≤
12	7, 10, 11	wbr 5070	. . . . 5 wff 𝑧 ≤ 𝑦
13	9, 12	wa 395	. . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)
14	13, 6, 4	crab 3067	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}
15	2, 3, 4, 4, 14	cmpo 7257	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})
16	1, 15	wceq 1539	1 wff (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})

This definition is referenced by:  iocval  13045  elioc1  13050  iocssxr  13092  iocssicc  13098  iocssioo  13100  ioounsn  13138  snunioc  13141  leordtval2  22271  iocpnfordt  22274  lecldbas  22278  pnfnei  22279  iocmnfcld  23838  xrtgioo  23875  ismbf3d  24723  dvloglem  25708  asindmre  35787  dvasin  35788  ioossioc  42920  eliocre  42937  lbioc  42941