MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ioc Structured version   Unicode version

Definition df-ioc 11647
Description: Define the set of open-below, closed-above intervals of extended reals. (Contributed by NM, 24-Dec-2006.)
Assertion
Ref Expression
df-ioc  |-  (,]  =  ( x  e.  RR* ,  y  e.  RR*  |->  { z  e.  RR*  |  (
x  <  z  /\  z  <_  y ) } )
Distinct variable group:    x, y, z

Detailed syntax breakdown of Definition df-ioc
StepHypRef Expression
1 cioc 11643 . 2  class  (,]
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 cxr 9681 . . 3  class  RR*
52cv 1436 . . . . . 6  class  x
6 vz . . . . . . 7  setvar  z
76cv 1436 . . . . . 6  class  z
8 clt 9682 . . . . . 6  class  <
95, 7, 8wbr 4423 . . . . 5  wff  x  < 
z
103cv 1436 . . . . . 6  class  y
11 cle 9683 . . . . . 6  class  <_
127, 10, 11wbr 4423 . . . . 5  wff  z  <_ 
y
139, 12wa 370 . . . 4  wff  ( x  <  z  /\  z  <_  y )
1413, 6, 4crab 2775 . . 3  class  { z  e.  RR*  |  (
x  <  z  /\  z  <_  y ) }
152, 3, 4, 4, 14cmpt2 6307 . 2  class  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <  z  /\  z  <_ 
y ) } )
161, 15wceq 1437 1  wff  (,]  =  ( x  e.  RR* ,  y  e.  RR*  |->  { z  e.  RR*  |  (
x  <  z  /\  z  <_  y ) } )
Colors of variables: wff setvar class
This definition is referenced by:  iocval  11680  elioc1  11685  iocssxr  11725  iocssicc  11729  iocssioo  11731  snunioc  11767  leordtval2  20226  iocpnfordt  20229  lecldbas  20233  pnfnei  20234  iocmnfcld  21787  xrtgioo  21822  ismbf3d  22608  dvloglem  23591  asindmre  31991  dvasin  31992  ioounsn  36064  ioossioc  37537  snunioo2  37555  eliocre  37558  lbioc  37563
  Copyright terms: Public domain W3C validator