Definition df-icc 13400

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 13396	. 2 class [,]
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11262	. . 3 class ℝ*
5	2	cv 1569	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1569	. . . . . 6 class 𝑧
8		cle 11264	. . . . . 6 class ≤
9	5, 7, 8	wbr 5111	. . . . 5 wff 𝑥 ≤ 𝑧
10	3	cv 1569	. . . . . 6 class 𝑦
11	7, 10, 8	wbr 5111	. . . . 5 wff 𝑧 ≤ 𝑦
12	9, 11	wa 401	. . . 4 wff (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)
13	12, 6, 4	crab 3418	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)}
14	2, 3, 4, 4, 13	cmpo 7422	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)})
15	1, 14	wceq 1570	1 wff [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)})

This definition is used by:  iccval  13432  elicc1  13437  iccss  13462  iccssioo  13463  iccss2  13465  iccssico  13466  iccssxr  13478  ioossicc  13481  icossicc  13484  iocssicc  13485  iccf  13496  ioounsn  13525  snunioo  13526  snunico  13527  snunioc  13528  ioodisj  13530  leordtval2  23424  iccordt  23426  lecldbas  23431  ioombl  25780  itgspliticc  26052  psercnlem2  26643  tanord1  26758  cvmliftlem10  35828  ftc1anclem7  38412  ftc1anclem8  38413  ftc1anc  38414  snunioo1  46306  iccin  49751  iccdisj2  49752