Definition df-icc 13390

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 13386	. 2 class [,]
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11291	. . 3 class ℝ*
5	2	cv 1535	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1535	. . . . . 6 class 𝑧
8		cle 11293	. . . . . 6 class ≤
9	5, 7, 8	wbr 5147	. . . . 5 wff 𝑥 ≤ 𝑧
10	3	cv 1535	. . . . . 6 class 𝑦
11	7, 10, 8	wbr 5147	. . . . 5 wff 𝑧 ≤ 𝑦
12	9, 11	wa 395	. . . 4 wff (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)
13	12, 6, 4	crab 3432	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)}
14	2, 3, 4, 4, 13	cmpo 7432	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)})
15	1, 14	wceq 1536	1 wff [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)})

This definition is referenced by:  iccval  13422  elicc1  13427  iccss  13451  iccssioo  13452  iccss2  13454  iccssico  13455  iccssxr  13466  ioossicc  13469  icossicc  13472  iocssicc  13473  iccf  13484  ioounsn  13513  snunioo  13514  snunico  13515  snunioc  13516  ioodisj  13518  leordtval2  23235  iccordt  23237  lecldbas  23242  ioombl  25613  itgspliticc  25886  psercnlem2  26482  tanord1  26593  cvmliftlem10  35278  ftc1anclem7  37685  ftc1anclem8  37686  ftc1anc  37687  snunioo1  45464  iccin  48692  iccdisj2  48693