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 12819
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 12815 . 2 class (,]
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cxr 10745 . . 3 class *
52cv 1541 . . . . . 6 class 𝑥
6 vz . . . . . . 7 setvar 𝑧
76cv 1541 . . . . . 6 class 𝑧
8 clt 10746 . . . . . 6 class <
95, 7, 8wbr 5027 . . . . 5 wff 𝑥 < 𝑧
103cv 1541 . . . . . 6 class 𝑦
11 cle 10747 . . . . . 6 class
127, 10, 11wbr 5027 . . . . 5 wff 𝑧𝑦
139, 12wa 399 . . . 4 wff (𝑥 < 𝑧𝑧𝑦)
1413, 6, 4crab 3057 . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧𝑦)}
152, 3, 4, 4, 14cmpo 7166 . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧𝑦)})
161, 15wceq 1542 1 wff (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧𝑦)})
Colors of variables: wff setvar class
This definition is referenced by:  iocval  12851  elioc1  12856  iocssxr  12898  iocssicc  12904  iocssioo  12906  ioounsn  12944  snunioc  12947  leordtval2  21956  iocpnfordt  21959  lecldbas  21963  pnfnei  21964  iocmnfcld  23514  xrtgioo  23551  ismbf3d  24399  dvloglem  25383  asindmre  35472  dvasin  35473  ioossioc  42554  eliocre  42571  lbioc  42575
  Copyright terms: Public domain W3C validator