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 12050
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 12046 . 2 class (,)
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cxr 9952 . . 3 class *
52cv 1474 . . . . . 6 class 𝑥
6 vz . . . . . . 7 setvar 𝑧
76cv 1474 . . . . . 6 class 𝑧
8 clt 9953 . . . . . 6 class <
95, 7, 8wbr 4583 . . . . 5 wff 𝑥 < 𝑧
103cv 1474 . . . . . 6 class 𝑦
117, 10, 8wbr 4583 . . . . 5 wff 𝑧 < 𝑦
129, 11wa 383 . . . 4 wff (𝑥 < 𝑧𝑧 < 𝑦)
1312, 6, 4crab 2900 . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)}
142, 3, 4, 4, 13cmpt2 6551 . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)})
151, 14wceq 1475 1 wff (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)})
Colors of variables: wff setvar class
This definition is referenced by:  iooex  12069  iooval  12070  ndmioo  12073  elioo3g  12075  iooin  12080  iooss1  12081  iooss2  12082  elioo1  12086  iccssioo  12113  ioossicc  12130  ioossico  12133  iocssioo  12134  icossioo  12135  ioossioo  12136  ioof  12142  snunioo  12169  ioodisj  12173  ioojoin  12174  ioopnfsup  12525  leordtval  20827  icopnfcld  22381  iocmnfcld  22382  bndth  22565  ioombl  23140  ioorf  23147  ioorinv2  23149  ismbf3d  23227  dvfsumrlimge0  23597  dvfsumrlim2  23599  tanord1  24087  dvloglem  24194  rlimcnp  24492  rlimcnp2  24493  dchrisum0lem2a  25006  pnt  25103  joiniooico  28926  tpr2rico  29286  asindmre  32665  dvasin  32666  ioounsn  36814  ioossioc  38560  snunioo2  38578  snunioo1  38585  ioossioobi  38590
  Copyright terms: Public domain W3C validator