Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-icc Structured version   Visualization version   GIF version

Definition df-icc 12595
 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
StepHypRef Expression
1 cicc 12591 . 2 class [,]
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cxr 10520 . . 3 class *
52cv 1521 . . . . . 6 class 𝑥
6 vz . . . . . . 7 setvar 𝑧
76cv 1521 . . . . . 6 class 𝑧
8 cle 10522 . . . . . 6 class
95, 7, 8wbr 4962 . . . . 5 wff 𝑥𝑧
103cv 1521 . . . . . 6 class 𝑦
117, 10, 8wbr 4962 . . . . 5 wff 𝑧𝑦
129, 11wa 396 . . . 4 wff (𝑥𝑧𝑧𝑦)
1312, 6, 4crab 3109 . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧𝑦)}
142, 3, 4, 4, 13cmpo 7018 . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧𝑦)})
151, 14wceq 1522 1 wff [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧𝑦)})
 Colors of variables: wff setvar class This definition is referenced by:  iccval  12627  elicc1  12632  iccss  12654  iccssioo  12655  iccss2  12657  iccssico  12658  iccssxr  12669  ioossicc  12672  icossicc  12674  iocssicc  12675  iccf  12686  ioounsn  12713  snunioo  12714  snunico  12715  snunioc  12716  ioodisj  12718  leordtval2  21504  iccordt  21506  lecldbas  21511  ioombl  23849  itgspliticc  24120  psercnlem2  24695  tanord1  24802  cvmliftlem10  32149  ftc1anclem7  34504  ftc1anclem8  34505  ftc1anc  34506  snunioo1  41330
 Copyright terms: Public domain W3C validator