Definition df-icc 12220

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 12216	. 2 class [,]
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 10111	. . 3 class ℝ*
5	2	cv 1522	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1522	. . . . . 6 class 𝑧
8		cle 10113	. . . . . 6 class ≤
9	5, 7, 8	wbr 4685	. . . . 5 wff 𝑥 ≤ 𝑧
10	3	cv 1522	. . . . . 6 class 𝑦
11	7, 10, 8	wbr 4685	. . . . 5 wff 𝑧 ≤ 𝑦
12	9, 11	wa 383	. . . 4 wff (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)
13	12, 6, 4	crab 2945	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)}
14	2, 3, 4, 4, 13	cmpt2 6692	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)})
15	1, 14	wceq 1523	1 wff [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)})

This definition is referenced by:  iccval  12252  elicc1  12257  iccss  12279  iccssioo  12280  iccss2  12282  iccssico  12283  iccssxr  12294  ioossicc  12297  icossicc  12298  iocssicc  12299  iccf  12310  snunioo  12336  snunico  12337  snunioc  12338  ioodisj  12340  leordtval2  21064  iccordt  21066  lecldbas  21071  ioombl  23379  itgspliticc  23648  psercnlem2  24223  tanord1  24328  cvmliftlem10  31402  ftc1anclem7  33621  ftc1anclem8  33622  ftc1anc  33623  ioounsn  38112  snunioo2  40049  snunioo1  40056