Definition df-icc 13430

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 13426	. 2 class [,]
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11291	. . 3 class ℝ*
5	2	cv 1569	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1569	. . . . . 6 class 𝑧
8		cle 11293	. . . . . 6 class ≤
9	5, 7, 8	wbr 5103	. . . . 5 wff 𝑥 ≤ 𝑧
10	3	cv 1569	. . . . . 6 class 𝑦
11	7, 10, 8	wbr 5103	. . . . 5 wff 𝑧 ≤ 𝑦
12	9, 11	wa 401	. . . 4 wff (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)
13	12, 6, 4	crab 3412	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)}
14	2, 3, 4, 4, 13	cmpo 7418	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)})
15	1, 14	wceq 1570	1 wff [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)})

This definition is used by:  iccval  13462  elicc1  13467  iccss  13492  iccssioo  13493  iccss2  13495  iccssico  13496  iccssxr  13508  ioossicc  13511  icossicc  13514  iocssicc  13515  iccf  13526  ioounsn  13555  snunioo  13556  snunico  13557  snunioc  13558  ioodisj  13560  leordtval2  23469  iccordt  23471  lecldbas  23476  ioombl  25825  itgspliticc  26096  psercnlem2  26692  tanord1  26806  cvmliftlem10  35956  ftc1anclem7  38513  ftc1anclem8  38514  ftc1anc  38515  snunioo1  46407  iccin  49887  iccdisj2  49888