MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ioc Structured version   Visualization version   GIF version

Definition df-ioc 12733
Description: Define the set of open-below, closed-above intervals of extended reals. (Contributed by NM, 24-Dec-2006.)
Assertion
Ref Expression
df-ioc (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧𝑦)})
Distinct variable group:   𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-ioc
StepHypRef Expression
1 cioc 12729 . 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 𝑦
11 cle 10665 . . . . . 6 class
127, 10, 11wbr 5058 . . . . 5 wff 𝑧𝑦
139, 12wa 396 . . . 4 wff (𝑥 < 𝑧𝑧𝑦)
1413, 6, 4crab 3142 . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧𝑦)}
152, 3, 4, 4, 14cmpo 7147 . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧𝑦)})
161, 15wceq 1528 1 wff (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧𝑦)})
Colors of variables: wff setvar class
This definition is referenced by:  iocval  12765  elioc1  12770  iocssxr  12810  iocssicc  12815  iocssioo  12817  ioounsn  12853  snunioc  12856  leordtval2  21750  iocpnfordt  21753  lecldbas  21757  pnfnei  21758  iocmnfcld  23306  xrtgioo  23343  ismbf3d  24184  dvloglem  25158  asindmre  34859  dvasin  34860  ioossioc  41646  eliocre  41665  lbioc  41669
  Copyright terms: Public domain W3C validator