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 12002
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 11998 . 2 class (,)
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cxr 9925 . . 3 class *
52cv 1473 . . . . . 6 class 𝑥
6 vz . . . . . . 7 setvar 𝑧
76cv 1473 . . . . . 6 class 𝑧
8 clt 9926 . . . . . 6 class <
95, 7, 8wbr 4573 . . . . 5 wff 𝑥 < 𝑧
103cv 1473 . . . . . 6 class 𝑦
117, 10, 8wbr 4573 . . . . 5 wff 𝑧 < 𝑦
129, 11wa 382 . . . 4 wff (𝑥 < 𝑧𝑧 < 𝑦)
1312, 6, 4crab 2895 . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)}
142, 3, 4, 4, 13cmpt2 6525 . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)})
151, 14wceq 1474 1 wff (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)})
Colors of variables: wff setvar class
This definition is referenced by:  iooex  12021  iooval  12022  ndmioo  12025  elioo3g  12027  iooin  12032  iooss1  12033  iooss2  12034  elioo1  12038  iccssioo  12065  ioossicc  12082  ioossico  12085  iocssioo  12086  icossioo  12087  ioossioo  12088  ioof  12094  snunioo  12121  ioodisj  12125  ioojoin  12126  ioopnfsup  12476  leordtval  20765  icopnfcld  22309  iocmnfcld  22310  bndth  22492  ioombl  23053  ioorf  23060  ioorinv2  23062  ismbf3d  23140  dvfsumrlimge0  23510  dvfsumrlim2  23512  tanord1  24000  dvloglem  24107  rlimcnp  24405  rlimcnp2  24406  dchrisum0lem2a  24919  pnt  25016  joiniooico  28728  tpr2rico  29088  asindmre  32464  dvasin  32465  ioounsn  36613  ioossioc  38360  snunioo2  38378  snunioo1  38385  ioossioobi  38390
  Copyright terms: Public domain W3C validator