Definition df-icc 13262

Description: Define the set of closed intervals of extended reals. (Contributed by NM, 24-Dec-2006.)

Assertion

Ref	Expression
df-icc	⊢ [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)})

Distinct variable group:   𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-icc

Step	Hyp	Ref	Expression
1		cicc 13258	. 2 class [,]
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11155	. . 3 class ℝ*
5	2	cv 1540	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1540	. . . . . 6 class 𝑧
8		cle 11157	. . . . . 6 class ≤
9	5, 7, 8	wbr 5095	. . . . 5 wff 𝑥 ≤ 𝑧
10	3	cv 1540	. . . . . 6 class 𝑦
11	7, 10, 8	wbr 5095	. . . . 5 wff 𝑧 ≤ 𝑦
12	9, 11	wa 395	. . . 4 wff (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)
13	12, 6, 4	crab 3397	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)}
14	2, 3, 4, 4, 13	cmpo 7357	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)})
15	1, 14	wceq 1541	1 wff [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)})

This definition is referenced by:  iccval  13294  elicc1  13299  iccss  13324  iccssioo  13325  iccss2  13327  iccssico  13328  iccssxr  13340  ioossicc  13343  icossicc  13346  iocssicc  13347  iccf  13358  ioounsn  13387  snunioo  13388  snunico  13389  snunioc  13390  ioodisj  13392  leordtval2  23137  iccordt  23139  lecldbas  23144  ioombl  25503  itgspliticc  25775  psercnlem2  26371  tanord1  26483  cvmliftlem10  35349  ftc1anclem7  37749  ftc1anclem8  37750  ftc1anc  37751  snunioo1  45626  iccin  49010  iccdisj2  49011