Definition df-icc 13383

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

This definition is used by:  iccval  13415  elicc1  13420  iccss  13445  iccssioo  13446  iccss2  13448  iccssico  13449  iccssxr  13461  ioossicc  13464  icossicc  13467  iocssicc  13468  iccf  13479  ioounsn  13508  snunioo  13509  snunico  13510  snunioc  13511  ioodisj  13513  leordtval2  23378  iccordt  23380  lecldbas  23385  ioombl  25733  itgspliticc  26005  psercnlem2  26596  tanord1  26711  cvmliftlem10  35794  ftc1anclem7  38378  ftc1anclem8  38379  ftc1anc  38380  snunioo1  46256  iccin  49702  iccdisj2  49703