Definition df-icc 13358

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 13354	. 2 class [,]
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11217	. . 3 class ℝ*
5	2	cv 1561	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1561	. . . . . 6 class 𝑧
8		cle 11219	. . . . . 6 class ≤
9	5, 7, 8	wbr 5102	. . . . 5 wff 𝑥 ≤ 𝑧
10	3	cv 1561	. . . . . 6 class 𝑦
11	7, 10, 8	wbr 5102	. . . . 5 wff 𝑧 ≤ 𝑦
12	9, 11	wa 399	. . . 4 wff (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)
13	12, 6, 4	crab 3416	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)}
14	2, 3, 4, 4, 13	cmpo 7400	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)})
15	1, 14	wceq 1562	1 wff [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)})

This definition is referenced by:  iccval  13390  elicc1  13395  iccss  13420  iccssioo  13421  iccss2  13423  iccssico  13424  iccssxr  13436  ioossicc  13439  icossicc  13442  iocssicc  13443  iccf  13454  ioounsn  13483  snunioo  13484  snunico  13485  snunioc  13486  ioodisj  13488  leordtval2  23274  iccordt  23276  lecldbas  23281  ioombl  25629  itgspliticc  25901  psercnlem2  26489  tanord1  26604  cvmliftlem10  35649  ftc1anclem7  38203  ftc1anclem8  38204  ftc1anc  38205  snunioo1  46093  iccin  49522  iccdisj2  49523