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 12004
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 12000 . 2 class (,]
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cxr 9926 . . 3 class *
52cv 1473 . . . . . 6 class 𝑥
6 vz . . . . . . 7 setvar 𝑧
76cv 1473 . . . . . 6 class 𝑧
8 clt 9927 . . . . . 6 class <
95, 7, 8wbr 4574 . . . . 5 wff 𝑥 < 𝑧
103cv 1473 . . . . . 6 class 𝑦
11 cle 9928 . . . . . 6 class
127, 10, 11wbr 4574 . . . . 5 wff 𝑧𝑦
139, 12wa 382 . . . 4 wff (𝑥 < 𝑧𝑧𝑦)
1413, 6, 4crab 2896 . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧𝑦)}
152, 3, 4, 4, 14cmpt2 6526 . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧𝑦)})
161, 15wceq 1474 1 wff (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧𝑦)})
Colors of variables: wff setvar class
This definition is referenced by:  iocval  12036  elioc1  12041  iocssxr  12081  iocssicc  12085  iocssioo  12087  snunioc  12124  leordtval2  20765  iocpnfordt  20768  lecldbas  20772  pnfnei  20773  iocmnfcld  22311  xrtgioo  22346  ismbf3d  23141  dvloglem  24108  asindmre  32465  dvasin  32466  ioounsn  36614  ioossioc  38361  snunioo2  38379  eliocre  38382  lbioc  38387
  Copyright terms: Public domain W3C validator