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 12735
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 12731 . 2 class [,]
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cxr 10663 . . 3 class *
52cv 1527 . . . . . 6 class 𝑥
6 vz . . . . . . 7 setvar 𝑧
76cv 1527 . . . . . 6 class 𝑧
8 cle 10665 . . . . . 6 class
95, 7, 8wbr 5058 . . . . 5 wff 𝑥𝑧
103cv 1527 . . . . . 6 class 𝑦
117, 10, 8wbr 5058 . . . . 5 wff 𝑧𝑦
129, 11wa 396 . . . 4 wff (𝑥𝑧𝑧𝑦)
1312, 6, 4crab 3142 . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧𝑦)}
142, 3, 4, 4, 13cmpo 7147 . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧𝑦)})
151, 14wceq 1528 1 wff [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧𝑦)})
Colors of variables: wff setvar class
This definition is referenced by:  iccval  12767  elicc1  12772  iccss  12794  iccssioo  12795  iccss2  12797  iccssico  12798  iccssxr  12809  ioossicc  12812  icossicc  12814  iocssicc  12815  iccf  12826  ioounsn  12853  snunioo  12854  snunico  12855  snunioc  12856  ioodisj  12858  leordtval2  21750  iccordt  21752  lecldbas  21757  ioombl  24095  itgspliticc  24366  psercnlem2  24941  tanord1  25048  cvmliftlem10  32439  ftc1anclem7  34855  ftc1anclem8  34856  ftc1anc  34857  snunioo1  41668
  Copyright terms: Public domain W3C validator