Definition df-ioc 13353

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 13349	. 2 class (,]
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11269	. . 3 class ℝ*
5	2	cv 1533	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1533	. . . . . 6 class 𝑧
8		clt 11270	. . . . . 6 class <
9	5, 7, 8	wbr 5142	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1533	. . . . . 6 class 𝑦
11		cle 11271	. . . . . 6 class ≤
12	7, 10, 11	wbr 5142	. . . . 5 wff 𝑧 ≤ 𝑦
13	9, 12	wa 395	. . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)
14	13, 6, 4	crab 3427	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}
15	2, 3, 4, 4, 14	cmpo 7416	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})
16	1, 15	wceq 1534	1 wff (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})

This definition is referenced by:  iocval  13385  elioc1  13390  iocssxr  13432  iocssicc  13438  iocssioo  13440  ioounsn  13478  snunioc  13481  leordtval2  23103  iocpnfordt  23106  lecldbas  23110  pnfnei  23111  iocmnfcld  24672  xrtgioo  24709  ismbf3d  25570  dvloglem  26569  asindmre  37111  dvasin  37112  ioossioc  44800  eliocre  44817  lbioc  44821