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 12176
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 12172 . 2 class (,)
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cxr 10070 . . 3 class *
52cv 1481 . . . . . 6 class 𝑥
6 vz . . . . . . 7 setvar 𝑧
76cv 1481 . . . . . 6 class 𝑧
8 clt 10071 . . . . . 6 class <
95, 7, 8wbr 4651 . . . . 5 wff 𝑥 < 𝑧
103cv 1481 . . . . . 6 class 𝑦
117, 10, 8wbr 4651 . . . . 5 wff 𝑧 < 𝑦
129, 11wa 384 . . . 4 wff (𝑥 < 𝑧𝑧 < 𝑦)
1312, 6, 4crab 2915 . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)}
142, 3, 4, 4, 13cmpt2 6649 . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)})
151, 14wceq 1482 1 wff (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)})
Colors of variables: wff setvar class
This definition is referenced by:  iooex  12195  iooval  12196  ndmioo  12199  elioo3g  12201  iooin  12206  iooss1  12207  iooss2  12208  elioo1  12212  iccssioo  12239  ioossicc  12256  ioossico  12259  iocssioo  12260  icossioo  12261  ioossioo  12262  ioof  12268  snunioo  12295  ioodisj  12299  ioojoin  12300  ioopnfsup  12658  leordtval  21011  icopnfcld  22565  iocmnfcld  22566  bndth  22751  ioombl  23327  ioorf  23335  ioorinv2  23337  ismbf3d  23415  dvfsumrlimge0  23787  dvfsumrlim2  23789  tanord1  24277  dvloglem  24388  rlimcnp  24686  rlimcnp2  24687  dchrisum0lem2a  25200  pnt  25297  joiniooico  29521  tpr2rico  29943  asindmre  33475  dvasin  33476  ioounsn  37621  ioossioc  39522  snunioo2  39540  snunioo1  39547  ioossioobi  39552
  Copyright terms: Public domain W3C validator