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 12818
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 12814 . 2 class (,)
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cxr 10745 . . 3 class *
52cv 1541 . . . . . 6 class 𝑥
6 vz . . . . . . 7 setvar 𝑧
76cv 1541 . . . . . 6 class 𝑧
8 clt 10746 . . . . . 6 class <
95, 7, 8wbr 5027 . . . . 5 wff 𝑥 < 𝑧
103cv 1541 . . . . . 6 class 𝑦
117, 10, 8wbr 5027 . . . . 5 wff 𝑧 < 𝑦
129, 11wa 399 . . . 4 wff (𝑥 < 𝑧𝑧 < 𝑦)
1312, 6, 4crab 3057 . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)}
142, 3, 4, 4, 13cmpo 7166 . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)})
151, 14wceq 1542 1 wff (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)})
Colors of variables: wff setvar class
This definition is referenced by:  iooex  12837  iooval  12838  ndmioo  12841  elioo3g  12843  iooin  12848  iooss1  12849  iooss2  12850  elioo1  12854  iccssioo  12883  ioossicc  12900  ioossico  12905  iocssioo  12906  icossioo  12907  ioossioo  12908  ioof  12914  ioounsn  12944  snunioo  12945  ioodisj  12949  ioojoin  12950  ioopnfsup  13316  leordtval  21957  icopnfcld  23513  iocmnfcld  23514  bndth  23703  ioombl  24310  ioorf  24318  ioorinv2  24320  ismbf3d  24399  dvfsumrlimge0  24774  dvfsumrlim2  24776  tanord1  25273  dvloglem  25383  rlimcnp  25695  rlimcnp2  25696  dchrisum0lem2a  26245  pnt  26342  joiniooico  30662  tpr2rico  31426  asindmre  35472  dvasin  35473  ioossioc  42554  snunioo1  42574  ioossioobi  42579
  Copyright terms: Public domain W3C validator