Definition df-icc 13379

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 13375	. 2 class [,]
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11242	. . 3 class ℝ*
5	2	cv 1566	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1566	. . . . . 6 class 𝑧
8		cle 11244	. . . . . 6 class ≤
9	5, 7, 8	wbr 5113	. . . . 5 wff 𝑥 ≤ 𝑧
10	3	cv 1566	. . . . . 6 class 𝑦
11	7, 10, 8	wbr 5113	. . . . 5 wff 𝑧 ≤ 𝑦
12	9, 11	wa 400	. . . 4 wff (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)
13	12, 6, 4	crab 3423	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)}
14	2, 3, 4, 4, 13	cmpo 7413	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)})
15	1, 14	wceq 1567	1 wff [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)})

This definition is referenced by:  iccval  13411  elicc1  13416  iccss  13441  iccssioo  13442  iccss2  13444  iccssico  13445  iccssxr  13457  ioossicc  13460  icossicc  13463  iocssicc  13464  iccf  13475  ioounsn  13504  snunioo  13505  snunico  13506  snunioc  13507  ioodisj  13509  leordtval2  23338  iccordt  23340  lecldbas  23345  ioombl  25693  itgspliticc  25965  psercnlem2  26553  tanord1  26668  cvmliftlem10  35719  ftc1anclem7  38272  ftc1anclem8  38273  ftc1anc  38274  snunioo1  46154  iccin  49593  iccdisj2  49594