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 12137
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 12133 . 2 class (,)
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cxr 10033 . . 3 class *
52cv 1479 . . . . . 6 class 𝑥
6 vz . . . . . . 7 setvar 𝑧
76cv 1479 . . . . . 6 class 𝑧
8 clt 10034 . . . . . 6 class <
95, 7, 8wbr 4623 . . . . 5 wff 𝑥 < 𝑧
103cv 1479 . . . . . 6 class 𝑦
117, 10, 8wbr 4623 . . . . 5 wff 𝑧 < 𝑦
129, 11wa 384 . . . 4 wff (𝑥 < 𝑧𝑧 < 𝑦)
1312, 6, 4crab 2912 . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)}
142, 3, 4, 4, 13cmpt2 6617 . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)})
151, 14wceq 1480 1 wff (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)})
Colors of variables: wff setvar class
This definition is referenced by:  iooex  12156  iooval  12157  ndmioo  12160  elioo3g  12162  iooin  12167  iooss1  12168  iooss2  12169  elioo1  12173  iccssioo  12200  ioossicc  12217  ioossico  12220  iocssioo  12221  icossioo  12222  ioossioo  12223  ioof  12229  snunioo  12256  ioodisj  12260  ioojoin  12261  ioopnfsup  12619  leordtval  20957  icopnfcld  22511  iocmnfcld  22512  bndth  22697  ioombl  23273  ioorf  23281  ioorinv2  23283  ismbf3d  23361  dvfsumrlimge0  23731  dvfsumrlim2  23733  tanord1  24221  dvloglem  24328  rlimcnp  24626  rlimcnp2  24627  dchrisum0lem2a  25140  pnt  25237  joiniooico  29421  tpr2rico  29782  asindmre  33166  dvasin  33167  ioounsn  37315  ioossioc  39159  snunioo2  39177  snunioo1  39184  ioossioobi  39189
  Copyright terms: Public domain W3C validator