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 13392
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 13388 . 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 𝑦
11 cle 11296 . . . . . 6 class
127, 10, 11wbr 5143 . . . . 5 wff 𝑧𝑦
139, 12wa 395 . . . 4 wff (𝑥 < 𝑧𝑧𝑦)
1413, 6, 4crab 3436 . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧𝑦)}
152, 3, 4, 4, 14cmpo 7433 . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧𝑦)})
161, 15wceq 1540 1 wff (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧𝑦)})
Colors of variables: wff setvar class
This definition is referenced by:  iocval  13424  elioc1  13429  iocssxr  13471  iocssicc  13477  iocssioo  13479  ioounsn  13517  snunioc  13520  leordtval2  23220  iocpnfordt  23223  lecldbas  23227  pnfnei  23228  iocmnfcld  24789  xrtgioo  24828  ismbf3d  25689  dvloglem  26690  asindmre  37710  dvasin  37711  iocioodisjd  42355  ioossioc  45505  eliocre  45522  lbioc  45526
  Copyright terms: Public domain W3C validator