Definition df-icc 13507

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

This definition is used by:  iccval  13539  elicc1  13544  iccss  13569  iccssioo  13570  iccss2  13572  iccssico  13573  iccssxr  13585  ioossicc  13588  icossicc  13591  iocssicc  13592  iccf  13603  ioounsn  13632  snunioo  13633  snunico  13634  snunioc  13635  ioodisj  13637  leordtval2  23557  iccordt  23559  lecldbas  23564  ioombl  25913  itgspliticc  26184  psercnlem2  26778  tanord1  26892  cvmliftlem10  36225  ftc1anclem7  38808  ftc1anclem8  38809  ftc1anc  38810  snunioo1  46727  iccin  50213  iccdisj2  50214