Definition df-ioc 13376

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 13372	. 2 class (,]
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11241	. . 3 class ℝ*
5	2	cv 1567	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1567	. . . . . 6 class 𝑧
8		clt 11242	. . . . . 6 class <
9	5, 7, 8	wbr 5108	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1567	. . . . . 6 class 𝑦
11		cle 11243	. . . . . 6 class ≤
12	7, 10, 11	wbr 5108	. . . . 5 wff 𝑧 ≤ 𝑦
13	9, 12	wa 400	. . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)
14	13, 6, 4	crab 3414	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}
15	2, 3, 4, 4, 14	cmpo 7412	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})
16	1, 15	wceq 1568	1 wff (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})

This definition is referenced by:  iocval  13408  elioc1  13413  iocssxr  13457  iocssicc  13463  iocssioo  13465  ioounsn  13503  snunioc  13506  leordtval2  23348  iocpnfordt  23351  lecldbas  23355  pnfnei  23356  iocmnfcld  24904  xrtgioo  24943  ismbf3d  25792  dvloglem  26789  asindmre  38320  dvasin  38321  iocioodisjd  43049  ioossioc  46178  eliocre  46195  lbioc  46199