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 12392
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 12388 . 2 class (,]
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cxr 10352 . . 3 class *
52cv 1636 . . . . . 6 class 𝑥
6 vz . . . . . . 7 setvar 𝑧
76cv 1636 . . . . . 6 class 𝑧
8 clt 10353 . . . . . 6 class <
95, 7, 8wbr 4837 . . . . 5 wff 𝑥 < 𝑧
103cv 1636 . . . . . 6 class 𝑦
11 cle 10354 . . . . . 6 class
127, 10, 11wbr 4837 . . . . 5 wff 𝑧𝑦
139, 12wa 384 . . . 4 wff (𝑥 < 𝑧𝑧𝑦)
1413, 6, 4crab 3096 . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧𝑦)}
152, 3, 4, 4, 14cmpt2 6870 . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧𝑦)})
161, 15wceq 1637 1 wff (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧𝑦)})
Colors of variables: wff setvar class
This definition is referenced by:  iocval  12424  elioc1  12429  iocssxr  12469  iocssicc  12474  iocssioo  12476  ioounsn  12513  ioounsnOLD  12514  snunioc  12517  leordtval2  21224  iocpnfordt  21227  lecldbas  21231  pnfnei  21232  iocmnfcld  22779  xrtgioo  22816  ismbf3d  23629  dvloglem  24602  asindmre  33801  dvasin  33802  ioossioc  40191  eliocre  40210  lbioc  40214
  Copyright terms: Public domain W3C validator