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 12053
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 12049 . 2 class [,]
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cxr 9952 . . 3 class *
52cv 1474 . . . . . 6 class 𝑥
6 vz . . . . . . 7 setvar 𝑧
76cv 1474 . . . . . 6 class 𝑧
8 cle 9954 . . . . . 6 class
95, 7, 8wbr 4583 . . . . 5 wff 𝑥𝑧
103cv 1474 . . . . . 6 class 𝑦
117, 10, 8wbr 4583 . . . . 5 wff 𝑧𝑦
129, 11wa 383 . . . 4 wff (𝑥𝑧𝑧𝑦)
1312, 6, 4crab 2900 . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧𝑦)}
142, 3, 4, 4, 13cmpt2 6551 . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧𝑦)})
151, 14wceq 1475 1 wff [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧𝑦)})
Colors of variables: wff setvar class
This definition is referenced by:  iccval  12085  elicc1  12090  iccss  12112  iccssioo  12113  iccss2  12115  iccssico  12116  iccssxr  12127  ioossicc  12130  icossicc  12131  iocssicc  12132  iccf  12143  snunioo  12169  snunico  12170  snunioc  12171  ioodisj  12173  leordtval2  20826  iccordt  20828  lecldbas  20833  ioombl  23140  itgspliticc  23409  psercnlem2  23982  tanord1  24087  cvmliftlem10  30530  ftc1anclem7  32661  ftc1anclem8  32662  ftc1anc  32663  ioounsn  36814  snunioo2  38578  snunioo1  38585
  Copyright terms: Public domain W3C validator