Definition df-icc 12595

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 12591	. 2 class [,]
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 10520	. . 3 class ℝ*
5	2	cv 1521	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1521	. . . . . 6 class 𝑧
8		cle 10522	. . . . . 6 class ≤
9	5, 7, 8	wbr 4962	. . . . 5 wff 𝑥 ≤ 𝑧
10	3	cv 1521	. . . . . 6 class 𝑦
11	7, 10, 8	wbr 4962	. . . . 5 wff 𝑧 ≤ 𝑦
12	9, 11	wa 396	. . . 4 wff (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)
13	12, 6, 4	crab 3109	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)}
14	2, 3, 4, 4, 13	cmpo 7018	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)})
15	1, 14	wceq 1522	1 wff [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)})

This definition is referenced by:  iccval  12627  elicc1  12632  iccss  12654  iccssioo  12655  iccss2  12657  iccssico  12658  iccssxr  12669  ioossicc  12672  icossicc  12674  iocssicc  12675  iccf  12686  ioounsn  12713  snunioo  12714  snunico  12715  snunioc  12716  ioodisj  12718  leordtval2  21504  iccordt  21506  lecldbas  21511  ioombl  23849  itgspliticc  24120  psercnlem2  24695  tanord1  24802  cvmliftlem10  32149  ftc1anclem7  34504  ftc1anclem8  34505  ftc1anc  34506  snunioo1  41330