Definition df-icc 13483

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

This definition is used by:  iccval  13515  elicc1  13520  iccss  13545  iccssioo  13546  iccss2  13548  iccssico  13549  iccssxr  13561  ioossicc  13564  icossicc  13567  iocssicc  13568  iccf  13579  ioounsn  13608  snunioo  13609  snunico  13610  snunioc  13611  ioodisj  13613  leordtval2  23530  iccordt  23532  lecldbas  23537  ioombl  25886  itgspliticc  26157  psercnlem2  26751  tanord1  26865  cvmliftlem10  36101  ftc1anclem7  38660  ftc1anclem8  38661  ftc1anc  38662  snunioo1  46566  iccin  50046  iccdisj2  50047