Definition df-icc 13313

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 13309	. 2 class [,]
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11229	. . 3 class ℝ*
5	2	cv 1540	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1540	. . . . . 6 class 𝑧
8		cle 11231	. . . . . 6 class ≤
9	5, 7, 8	wbr 5141	. . . . 5 wff 𝑥 ≤ 𝑧
10	3	cv 1540	. . . . . 6 class 𝑦
11	7, 10, 8	wbr 5141	. . . . 5 wff 𝑧 ≤ 𝑦
12	9, 11	wa 396	. . . 4 wff (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)
13	12, 6, 4	crab 3431	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)}
14	2, 3, 4, 4, 13	cmpo 7395	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)})
15	1, 14	wceq 1541	1 wff [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)})

This definition is referenced by:  iccval  13345  elicc1  13350  iccss  13374  iccssioo  13375  iccss2  13377  iccssico  13378  iccssxr  13389  ioossicc  13392  icossicc  13395  iocssicc  13396  iccf  13407  ioounsn  13436  snunioo  13437  snunico  13438  snunioc  13439  ioodisj  13441  leordtval2  22645  iccordt  22647  lecldbas  22652  ioombl  25011  itgspliticc  25283  psercnlem2  25865  tanord1  25975  cvmliftlem10  34116  ftc1anclem7  36371  ftc1anclem8  36372  ftc1anc  36373  snunioo1  43998  iccin  47177  iccdisj2  47178