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 13391
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 13387 . 2 class (,)
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cxr 11294 . . 3 class *
52cv 1539 . . . . . 6 class 𝑥
6 vz . . . . . . 7 setvar 𝑧
76cv 1539 . . . . . 6 class 𝑧
8 clt 11295 . . . . . 6 class <
95, 7, 8wbr 5143 . . . . 5 wff 𝑥 < 𝑧
103cv 1539 . . . . . 6 class 𝑦
117, 10, 8wbr 5143 . . . . 5 wff 𝑧 < 𝑦
129, 11wa 395 . . . 4 wff (𝑥 < 𝑧𝑧 < 𝑦)
1312, 6, 4crab 3436 . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)}
142, 3, 4, 4, 13cmpo 7433 . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)})
151, 14wceq 1540 1 wff (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)})
Colors of variables: wff setvar class
This definition is referenced by:  iooex  13410  iooval  13411  ndmioo  13414  elioo3g  13416  iooin  13421  iooss1  13422  iooss2  13423  elioo1  13427  iccssioo  13456  ioossicc  13473  ioossico  13478  iocssioo  13479  icossioo  13480  ioossioo  13481  ioof  13487  ioounsn  13517  snunioo  13518  ioodisj  13522  ioojoin  13523  ioopnfsup  13904  leordtval  23221  icopnfcld  24788  iocmnfcld  24789  bndth  24990  ioombl  25600  ioorf  25608  ioorinv2  25610  ismbf3d  25689  dvfsumrlimge0  26071  dvfsumrlim2  26073  tanord1  26579  dvloglem  26690  rlimcnp  27008  rlimcnp2  27009  dchrisum0lem2a  27561  pnt  27658  joiniooico  32776  tpr2rico  33911  asindmre  37710  dvasin  37711  iocioodisjd  42355  ioossioc  45505  snunioo1  45525  ioossioobi  45530
  Copyright terms: Public domain W3C validator