Definition df-icc 13414

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 13410	. 2 class [,]
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11323	. . 3 class ℝ*
5	2	cv 1536	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1536	. . . . . 6 class 𝑧
8		cle 11325	. . . . . 6 class ≤
9	5, 7, 8	wbr 5166	. . . . 5 wff 𝑥 ≤ 𝑧
10	3	cv 1536	. . . . . 6 class 𝑦
11	7, 10, 8	wbr 5166	. . . . 5 wff 𝑧 ≤ 𝑦
12	9, 11	wa 395	. . . 4 wff (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)
13	12, 6, 4	crab 3443	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)}
14	2, 3, 4, 4, 13	cmpo 7450	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)})
15	1, 14	wceq 1537	1 wff [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)})

This definition is referenced by:  iccval  13446  elicc1  13451  iccss  13475  iccssioo  13476  iccss2  13478  iccssico  13479  iccssxr  13490  ioossicc  13493  icossicc  13496  iocssicc  13497  iccf  13508  ioounsn  13537  snunioo  13538  snunico  13539  snunioc  13540  ioodisj  13542  leordtval2  23241  iccordt  23243  lecldbas  23248  ioombl  25619  itgspliticc  25892  psercnlem2  26486  tanord1  26597  cvmliftlem10  35262  ftc1anclem7  37659  ftc1anclem8  37660  ftc1anc  37661  snunioo1  45430  iccin  48576  iccdisj2  48577