Definition df-icc 13015

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 13011	. 2 class [,]
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 10939	. . 3 class ℝ*
5	2	cv 1538	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1538	. . . . . 6 class 𝑧
8		cle 10941	. . . . . 6 class ≤
9	5, 7, 8	wbr 5070	. . . . 5 wff 𝑥 ≤ 𝑧
10	3	cv 1538	. . . . . 6 class 𝑦
11	7, 10, 8	wbr 5070	. . . . 5 wff 𝑧 ≤ 𝑦
12	9, 11	wa 395	. . . 4 wff (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)
13	12, 6, 4	crab 3067	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)}
14	2, 3, 4, 4, 13	cmpo 7257	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)})
15	1, 14	wceq 1539	1 wff [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)})

This definition is referenced by:  iccval  13047  elicc1  13052  iccss  13076  iccssioo  13077  iccss2  13079  iccssico  13080  iccssxr  13091  ioossicc  13094  icossicc  13097  iocssicc  13098  iccf  13109  ioounsn  13138  snunioo  13139  snunico  13140  snunioc  13141  ioodisj  13143  leordtval2  22271  iccordt  22273  lecldbas  22278  ioombl  24634  itgspliticc  24906  psercnlem2  25488  tanord1  25598  cvmliftlem10  33156  ftc1anclem7  35783  ftc1anclem8  35784  ftc1anc  35785  snunioo1  42940  iccin  46078  iccdisj2  46079