Definition df-ioc 13364

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 13360	. 2 class (,]
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11226	. . 3 class ℝ*
5	2	cv 1560	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1560	. . . . . 6 class 𝑧
8		clt 11227	. . . . . 6 class <
9	5, 7, 8	wbr 5101	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1560	. . . . . 6 class 𝑦
11		cle 11228	. . . . . 6 class ≤
12	7, 10, 11	wbr 5101	. . . . 5 wff 𝑧 ≤ 𝑦
13	9, 12	wa 399	. . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)
14	13, 6, 4	crab 3415	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}
15	2, 3, 4, 4, 14	cmpo 7398	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})
16	1, 15	wceq 1561	1 wff (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})

This definition is referenced by:  iocval  13396  elioc1  13401  iocssxr  13445  iocssicc  13451  iocssioo  13453  ioounsn  13491  snunioc  13494  leordtval2  23279  iocpnfordt  23282  lecldbas  23286  pnfnei  23287  iocmnfcld  24835  xrtgioo  24874  ismbf3d  25723  dvloglem  26720  asindmre  38207  dvasin  38208  iocioodisjd  42934  ioossioc  46059  eliocre  46076  lbioc  46080