Definition df-icc 12746

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

This definition is referenced by:  iccval  12778  elicc1  12783  iccss  12805  iccssioo  12806  iccss2  12808  iccssico  12809  iccssxr  12820  ioossicc  12823  icossicc  12825  iocssicc  12826  iccf  12837  ioounsn  12864  snunioo  12865  snunico  12866  snunioc  12867  ioodisj  12869  leordtval2  21820  iccordt  21822  lecldbas  21827  ioombl  24166  itgspliticc  24437  psercnlem2  25012  tanord1  25121  cvmliftlem10  32541  ftc1anclem7  34988  ftc1anclem8  34989  ftc1anc  34990  snunioo1  41837