Definition df-icc 13394

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

This definition is referenced by:  iccval  13426  elicc1  13431  iccss  13455  iccssioo  13456  iccss2  13458  iccssico  13459  iccssxr  13470  ioossicc  13473  icossicc  13476  iocssicc  13477  iccf  13488  ioounsn  13517  snunioo  13518  snunico  13519  snunioc  13520  ioodisj  13522  leordtval2  23220  iccordt  23222  lecldbas  23227  ioombl  25600  itgspliticc  25872  psercnlem2  26468  tanord1  26579  cvmliftlem10  35299  ftc1anclem7  37706  ftc1anclem8  37707  ftc1anc  37708  snunioo1  45525  iccin  48794  iccdisj2  48795