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 12051
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 12047 . 2 class (,]
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cxr 9952 . . 3 class *
52cv 1474 . . . . . 6 class 𝑥
6 vz . . . . . . 7 setvar 𝑧
76cv 1474 . . . . . 6 class 𝑧
8 clt 9953 . . . . . 6 class <
95, 7, 8wbr 4583 . . . . 5 wff 𝑥 < 𝑧
103cv 1474 . . . . . 6 class 𝑦
11 cle 9954 . . . . . 6 class
127, 10, 11wbr 4583 . . . . 5 wff 𝑧𝑦
139, 12wa 383 . . . 4 wff (𝑥 < 𝑧𝑧𝑦)
1413, 6, 4crab 2900 . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧𝑦)}
152, 3, 4, 4, 14cmpt2 6551 . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧𝑦)})
161, 15wceq 1475 1 wff (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧𝑦)})
Colors of variables: wff setvar class
This definition is referenced by:  iocval  12083  elioc1  12088  iocssxr  12128  iocssicc  12132  iocssioo  12134  snunioc  12171  leordtval2  20826  iocpnfordt  20829  lecldbas  20833  pnfnei  20834  iocmnfcld  22382  xrtgioo  22417  ismbf3d  23227  dvloglem  24194  asindmre  32665  dvasin  32666  ioounsn  36814  ioossioc  38560  snunioo2  38578  eliocre  38581  lbioc  38586
  Copyright terms: Public domain W3C validator