Definition df-icc 13289

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

This definition is referenced by:  iccval  13321  elicc1  13326  iccss  13351  iccssioo  13352  iccss2  13354  iccssico  13355  iccssxr  13367  ioossicc  13370  icossicc  13373  iocssicc  13374  iccf  13385  ioounsn  13414  snunioo  13415  snunico  13416  snunioc  13417  ioodisj  13419  leordtval2  23075  iccordt  23077  lecldbas  23082  ioombl  25442  itgspliticc  25714  psercnlem2  26310  tanord1  26422  cvmliftlem10  35254  ftc1anclem7  37666  ftc1anclem8  37667  ftc1anc  37668  snunioo1  45483  iccin  48857  iccdisj2  48858