Definition df-icc 13331

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 13327	. 2 class [,]
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11247	. . 3 class ℝ*
5	2	cv 1541	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1541	. . . . . 6 class 𝑧
8		cle 11249	. . . . . 6 class ≤
9	5, 7, 8	wbr 5149	. . . . 5 wff 𝑥 ≤ 𝑧
10	3	cv 1541	. . . . . 6 class 𝑦
11	7, 10, 8	wbr 5149	. . . . 5 wff 𝑧 ≤ 𝑦
12	9, 11	wa 397	. . . 4 wff (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)
13	12, 6, 4	crab 3433	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)}
14	2, 3, 4, 4, 13	cmpo 7411	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)})
15	1, 14	wceq 1542	1 wff [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)})

This definition is referenced by:  iccval  13363  elicc1  13368  iccss  13392  iccssioo  13393  iccss2  13395  iccssico  13396  iccssxr  13407  ioossicc  13410  icossicc  13413  iocssicc  13414  iccf  13425  ioounsn  13454  snunioo  13455  snunico  13456  snunioc  13457  ioodisj  13459  leordtval2  22716  iccordt  22718  lecldbas  22723  ioombl  25082  itgspliticc  25354  psercnlem2  25936  tanord1  26046  cvmliftlem10  34285  ftc1anclem7  36567  ftc1anclem8  36568  ftc1anc  36569  snunioo1  44225  iccin  47529  iccdisj2  47530