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 13323
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 13319 . 2 class (,)
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cxr 11242 . . 3 class *
52cv 1541 . . . . . 6 class 𝑥
6 vz . . . . . . 7 setvar 𝑧
76cv 1541 . . . . . 6 class 𝑧
8 clt 11243 . . . . . 6 class <
95, 7, 8wbr 5146 . . . . 5 wff 𝑥 < 𝑧
103cv 1541 . . . . . 6 class 𝑦
117, 10, 8wbr 5146 . . . . 5 wff 𝑧 < 𝑦
129, 11wa 397 . . . 4 wff (𝑥 < 𝑧𝑧 < 𝑦)
1312, 6, 4crab 3433 . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)}
142, 3, 4, 4, 13cmpo 7405 . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)})
151, 14wceq 1542 1 wff (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)})
Colors of variables: wff setvar class
This definition is referenced by:  iooex  13342  iooval  13343  ndmioo  13346  elioo3g  13348  iooin  13353  iooss1  13354  iooss2  13355  elioo1  13359  iccssioo  13388  ioossicc  13405  ioossico  13410  iocssioo  13411  icossioo  13412  ioossioo  13413  ioof  13419  ioounsn  13449  snunioo  13450  ioodisj  13454  ioojoin  13455  ioopnfsup  13824  leordtval  22698  icopnfcld  24265  iocmnfcld  24266  bndth  24455  ioombl  25063  ioorf  25071  ioorinv2  25073  ismbf3d  25152  dvfsumrlimge0  25528  dvfsumrlim2  25530  tanord1  26027  dvloglem  26137  rlimcnp  26449  rlimcnp2  26450  dchrisum0lem2a  26999  pnt  27096  joiniooico  31962  tpr2rico  32829  asindmre  36508  dvasin  36509  ioossioc  44139  snunioo1  44159  ioossioobi  44164
  Copyright terms: Public domain W3C validator