Definition df-icc 13297

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 13293	. 2 class [,]
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11170	. . 3 class ℝ*
5	2	cv 1546	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1546	. . . . . 6 class 𝑧
8		cle 11172	. . . . . 6 class ≤
9	5, 7, 8	wbr 5073	. . . . 5 wff 𝑥 ≤ 𝑧
10	3	cv 1546	. . . . . 6 class 𝑦
11	7, 10, 8	wbr 5073	. . . . 5 wff 𝑧 ≤ 𝑦
12	9, 11	wa 396	. . . 4 wff (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)
13	12, 6, 4	crab 3391	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)}
14	2, 3, 4, 4, 13	cmpo 7359	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)})
15	1, 14	wceq 1547	1 wff [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)})

This definition is referenced by:  iccval  13329  elicc1  13334  iccss  13359  iccssioo  13360  iccss2  13362  iccssico  13363  iccssxr  13375  ioossicc  13378  icossicc  13381  iocssicc  13382  iccf  13393  ioounsn  13422  snunioo  13423  snunico  13424  snunioc  13425  ioodisj  13427  leordtval2  23196  iccordt  23198  lecldbas  23203  ioombl  25551  itgspliticc  25823  psercnlem2  26408  tanord1  26520  cvmliftlem10  35531  ftc1anclem7  38075  ftc1anclem8  38076  ftc1anc  38077  snunioo1  45965  iccin  49394  iccdisj2  49395