Definition df-ioc 13093

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 13089	. 2 class (,]
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11017	. . 3 class ℝ*
5	2	cv 1538	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1538	. . . . . 6 class 𝑧
8		clt 11018	. . . . . 6 class <
9	5, 7, 8	wbr 5075	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1538	. . . . . 6 class 𝑦
11		cle 11019	. . . . . 6 class ≤
12	7, 10, 11	wbr 5075	. . . . 5 wff 𝑧 ≤ 𝑦
13	9, 12	wa 396	. . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)
14	13, 6, 4	crab 3069	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}
15	2, 3, 4, 4, 14	cmpo 7286	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})
16	1, 15	wceq 1539	1 wff (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})

This definition is referenced by:  iocval  13125  elioc1  13130  iocssxr  13172  iocssicc  13178  iocssioo  13180  ioounsn  13218  snunioc  13221  leordtval2  22372  iocpnfordt  22375  lecldbas  22379  pnfnei  22380  iocmnfcld  23941  xrtgioo  23978  ismbf3d  24827  dvloglem  25812  asindmre  35869  dvasin  35870  ioossioc  43037  eliocre  43054  lbioc  43058