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 12732
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 12728 . 2 class (,)
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cxr 10663 . . 3 class *
52cv 1527 . . . . . 6 class 𝑥
6 vz . . . . . . 7 setvar 𝑧
76cv 1527 . . . . . 6 class 𝑧
8 clt 10664 . . . . . 6 class <
95, 7, 8wbr 5058 . . . . 5 wff 𝑥 < 𝑧
103cv 1527 . . . . . 6 class 𝑦
117, 10, 8wbr 5058 . . . . 5 wff 𝑧 < 𝑦
129, 11wa 396 . . . 4 wff (𝑥 < 𝑧𝑧 < 𝑦)
1312, 6, 4crab 3142 . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)}
142, 3, 4, 4, 13cmpo 7147 . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)})
151, 14wceq 1528 1 wff (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)})
Colors of variables: wff setvar class
This definition is referenced by:  iooex  12751  iooval  12752  ndmioo  12755  elioo3g  12757  iooin  12762  iooss1  12763  iooss2  12764  elioo1  12768  iccssioo  12795  ioossicc  12812  ioossico  12816  iocssioo  12817  icossioo  12818  ioossioo  12819  ioof  12825  ioounsn  12853  snunioo  12854  ioodisj  12858  ioojoin  12859  ioopnfsup  13222  leordtval  21751  icopnfcld  23305  iocmnfcld  23306  bndth  23491  ioombl  24095  ioorf  24103  ioorinv2  24105  ismbf3d  24184  dvfsumrlimge0  24556  dvfsumrlim2  24558  tanord1  25048  dvloglem  25158  rlimcnp  25471  rlimcnp2  25472  dchrisum0lem2a  26021  pnt  26118  joiniooico  30424  tpr2rico  31055  asindmre  34859  dvasin  34860  ioossioc  41646  snunioo1  41668  ioossioobi  41673
  Copyright terms: Public domain W3C validator