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

Definition df-ioo 12372
Description: Define the set of open intervals of extended reals. (Contributed by NM, 24-Dec-2006.)
Assertion
Ref Expression
df-ioo (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)})
Distinct variable group:   𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-ioo
StepHypRef Expression
1 cioo 12368 . 2 class (,)
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cxr 10265 . . 3 class *
52cv 1631 . . . . . 6 class 𝑥
6 vz . . . . . . 7 setvar 𝑧
76cv 1631 . . . . . 6 class 𝑧
8 clt 10266 . . . . . 6 class <
95, 7, 8wbr 4804 . . . . 5 wff 𝑥 < 𝑧
103cv 1631 . . . . . 6 class 𝑦
117, 10, 8wbr 4804 . . . . 5 wff 𝑧 < 𝑦
129, 11wa 383 . . . 4 wff (𝑥 < 𝑧𝑧 < 𝑦)
1312, 6, 4crab 3054 . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)}
142, 3, 4, 4, 13cmpt2 6815 . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)})
151, 14wceq 1632 1 wff (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)})
Colors of variables: wff setvar class
This definition is referenced by:  iooex  12391  iooval  12392  ndmioo  12395  elioo3g  12397  iooin  12402  iooss1  12403  iooss2  12404  elioo1  12408  iccssioo  12435  ioossicc  12452  ioossico  12455  iocssioo  12456  icossioo  12457  ioossioo  12458  ioof  12464  snunioo  12491  ioodisj  12495  ioojoin  12496  ioopnfsup  12857  leordtval  21219  icopnfcld  22772  iocmnfcld  22773  bndth  22958  ioombl  23533  ioorf  23541  ioorinv2  23543  ismbf3d  23620  dvfsumrlimge0  23992  dvfsumrlim2  23994  tanord1  24482  dvloglem  24593  rlimcnp  24891  rlimcnp2  24892  dchrisum0lem2a  25405  pnt  25502  joiniooico  29845  tpr2rico  30267  asindmre  33808  dvasin  33809  ioounsn  38297  ioossioc  40216  snunioo2  40234  snunioo1  40241  ioossioobi  40246
  Copyright terms: Public domain W3C validator