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

Definition df-icc 12220
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 12216 . 2 class [,]
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cxr 10111 . . 3 class *
52cv 1522 . . . . . 6 class 𝑥
6 vz . . . . . . 7 setvar 𝑧
76cv 1522 . . . . . 6 class 𝑧
8 cle 10113 . . . . . 6 class
95, 7, 8wbr 4685 . . . . 5 wff 𝑥𝑧
103cv 1522 . . . . . 6 class 𝑦
117, 10, 8wbr 4685 . . . . 5 wff 𝑧𝑦
129, 11wa 383 . . . 4 wff (𝑥𝑧𝑧𝑦)
1312, 6, 4crab 2945 . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧𝑦)}
142, 3, 4, 4, 13cmpt2 6692 . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧𝑦)})
151, 14wceq 1523 1 wff [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧𝑦)})
Colors of variables: wff setvar class
This definition is referenced by:  iccval  12252  elicc1  12257  iccss  12279  iccssioo  12280  iccss2  12282  iccssico  12283  iccssxr  12294  ioossicc  12297  icossicc  12298  iocssicc  12299  iccf  12310  snunioo  12336  snunico  12337  snunioc  12338  ioodisj  12340  leordtval2  21064  iccordt  21066  lecldbas  21071  ioombl  23379  itgspliticc  23648  psercnlem2  24223  tanord1  24328  cvmliftlem10  31402  ftc1anclem7  33621  ftc1anclem8  33622  ftc1anc  33623  ioounsn  38112  snunioo2  40049  snunioo1  40056
  Copyright terms: Public domain W3C validator