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 12733
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 12729 . 2 class (,]
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cxr 10663 . . 3 class *
52cv 1529 . . . . . 6 class 𝑥
6 vz . . . . . . 7 setvar 𝑧
76cv 1529 . . . . . 6 class 𝑧
8 clt 10664 . . . . . 6 class <
95, 7, 8wbr 5063 . . . . 5 wff 𝑥 < 𝑧
103cv 1529 . . . . . 6 class 𝑦
11 cle 10665 . . . . . 6 class
127, 10, 11wbr 5063 . . . . 5 wff 𝑧𝑦
139, 12wa 396 . . . 4 wff (𝑥 < 𝑧𝑧𝑦)
1413, 6, 4crab 3147 . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧𝑦)}
152, 3, 4, 4, 14cmpo 7150 . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧𝑦)})
161, 15wceq 1530 1 wff (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧𝑦)})
Colors of variables: wff setvar class
This definition is referenced by:  iocval  12765  elioc1  12770  iocssxr  12810  iocssicc  12815  iocssioo  12817  ioounsn  12853  snunioc  12856  leordtval2  21736  iocpnfordt  21739  lecldbas  21743  pnfnei  21744  iocmnfcld  23292  xrtgioo  23329  ismbf3d  24170  dvloglem  25144  asindmre  34844  dvasin  34845  ioossioc  41631  eliocre  41650  lbioc  41654
  Copyright terms: Public domain W3C validator