Definition df-icc 13095

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

This definition is referenced by:  iccval  13127  elicc1  13132  iccss  13156  iccssioo  13157  iccss2  13159  iccssico  13160  iccssxr  13171  ioossicc  13174  icossicc  13177  iocssicc  13178  iccf  13189  ioounsn  13218  snunioo  13219  snunico  13220  snunioc  13221  ioodisj  13223  leordtval2  22372  iccordt  22374  lecldbas  22379  ioombl  24738  itgspliticc  25010  psercnlem2  25592  tanord1  25702  cvmliftlem10  33265  ftc1anclem7  35865  ftc1anclem8  35866  ftc1anc  35867  snunioo1  43057  iccin  46201  iccdisj2  46202