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 12734
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 12730 . 2 class (,)
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cxr 10666 . . 3 class *
52cv 1530 . . . . . 6 class 𝑥
6 vz . . . . . . 7 setvar 𝑧
76cv 1530 . . . . . 6 class 𝑧
8 clt 10667 . . . . . 6 class <
95, 7, 8wbr 5057 . . . . 5 wff 𝑥 < 𝑧
103cv 1530 . . . . . 6 class 𝑦
117, 10, 8wbr 5057 . . . . 5 wff 𝑧 < 𝑦
129, 11wa 398 . . . 4 wff (𝑥 < 𝑧𝑧 < 𝑦)
1312, 6, 4crab 3140 . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)}
142, 3, 4, 4, 13cmpo 7150 . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)})
151, 14wceq 1531 1 wff (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)})
Colors of variables: wff setvar class
This definition is referenced by:  iooex  12753  iooval  12754  ndmioo  12757  elioo3g  12759  iooin  12764  iooss1  12765  iooss2  12766  elioo1  12770  iccssioo  12797  ioossicc  12814  ioossico  12818  iocssioo  12819  icossioo  12820  ioossioo  12821  ioof  12827  ioounsn  12855  snunioo  12856  ioodisj  12860  ioojoin  12861  ioopnfsup  13224  leordtval  21813  icopnfcld  23368  iocmnfcld  23369  bndth  23554  ioombl  24158  ioorf  24166  ioorinv2  24168  ismbf3d  24247  dvfsumrlimge0  24619  dvfsumrlim2  24621  tanord1  25113  dvloglem  25223  rlimcnp  25535  rlimcnp2  25536  dchrisum0lem2a  26085  pnt  26182  joiniooico  30489  tpr2rico  31148  asindmre  34969  dvasin  34970  ioossioc  41755  snunioo1  41777  ioossioobi  41782
  Copyright terms: Public domain W3C validator