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 12397
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 12393 . 2 class (,)
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cxr 10358 . . 3 class *
52cv 1636 . . . . . 6 class 𝑥
6 vz . . . . . . 7 setvar 𝑧
76cv 1636 . . . . . 6 class 𝑧
8 clt 10359 . . . . . 6 class <
95, 7, 8wbr 4844 . . . . 5 wff 𝑥 < 𝑧
103cv 1636 . . . . . 6 class 𝑦
117, 10, 8wbr 4844 . . . . 5 wff 𝑧 < 𝑦
129, 11wa 384 . . . 4 wff (𝑥 < 𝑧𝑧 < 𝑦)
1312, 6, 4crab 3100 . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)}
142, 3, 4, 4, 13cmpt2 6876 . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)})
151, 14wceq 1637 1 wff (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)})
Colors of variables: wff setvar class
This definition is referenced by:  iooex  12416  iooval  12417  ndmioo  12420  elioo3g  12422  iooin  12427  iooss1  12428  iooss2  12429  elioo1  12433  iccssioo  12460  ioossicc  12477  ioossico  12481  iocssioo  12482  icossioo  12483  ioossioo  12484  ioof  12490  ioounsn  12519  ioounsnOLD  12520  snunioo  12521  ioodisj  12525  ioojoin  12526  ioopnfsup  12887  leordtval  21231  icopnfcld  22784  iocmnfcld  22785  bndth  22970  ioombl  23546  ioorf  23554  ioorinv2  23556  ismbf3d  23635  dvfsumrlimge0  24007  dvfsumrlim2  24009  tanord1  24498  dvloglem  24608  rlimcnp  24906  rlimcnp2  24907  dchrisum0lem2a  25420  pnt  25517  joiniooico  29863  tpr2rico  30283  asindmre  33807  dvasin  33808  ioossioc  40197  snunioo1  40219  ioossioobi  40224
  Copyright terms: Public domain W3C validator