Definition df-ioc 13297

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 13293	. 2 class (,]
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11172	. . 3 class ℝ*
5	2	cv 1542	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1542	. . . . . 6 class 𝑧
8		clt 11173	. . . . . 6 class <
9	5, 7, 8	wbr 5075	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1542	. . . . . 6 class 𝑦
11		cle 11174	. . . . . 6 class ≤
12	7, 10, 11	wbr 5075	. . . . 5 wff 𝑧 ≤ 𝑦
13	9, 12	wa 396	. . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)
14	13, 6, 4	crab 3388	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}
15	2, 3, 4, 4, 14	cmpo 7361	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})
16	1, 15	wceq 1543	1 wff (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})

This definition is referenced by:  iocval  13329  elioc1  13334  iocssxr  13378  iocssicc  13384  iocssioo  13386  ioounsn  13424  snunioc  13427  leordtval2  23198  iocpnfordt  23201  lecldbas  23205  pnfnei  23206  iocmnfcld  24754  xrtgioo  24793  ismbf3d  25642  dvloglem  26633  asindmre  38067  dvasin  38068  iocioodisjd  42794  ioossioc  45934  eliocre  45951  lbioc  45955