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 12165
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 12161 . 2 class (,]
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cxr 10058 . . 3 class *
52cv 1480 . . . . . 6 class 𝑥
6 vz . . . . . . 7 setvar 𝑧
76cv 1480 . . . . . 6 class 𝑧
8 clt 10059 . . . . . 6 class <
95, 7, 8wbr 4644 . . . . 5 wff 𝑥 < 𝑧
103cv 1480 . . . . . 6 class 𝑦
11 cle 10060 . . . . . 6 class
127, 10, 11wbr 4644 . . . . 5 wff 𝑧𝑦
139, 12wa 384 . . . 4 wff (𝑥 < 𝑧𝑧𝑦)
1413, 6, 4crab 2913 . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧𝑦)}
152, 3, 4, 4, 14cmpt2 6637 . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧𝑦)})
161, 15wceq 1481 1 wff (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧𝑦)})
Colors of variables: wff setvar class
This definition is referenced by:  iocval  12197  elioc1  12202  iocssxr  12242  iocssicc  12246  iocssioo  12248  snunioc  12285  leordtval2  20997  iocpnfordt  21000  lecldbas  21004  pnfnei  21005  iocmnfcld  22553  xrtgioo  22590  ismbf3d  23402  dvloglem  24375  asindmre  33466  dvasin  33467  ioounsn  37614  ioossioc  39516  snunioo2  39534  eliocre  39537  lbioc  39542
  Copyright terms: Public domain W3C validator