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

Definition df-ioc 11293
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 11289 . 2  class  (,]
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 cxr 9405 . . 3  class  RR*
52cv 1361 . . . . . 6  class  x
6 vz . . . . . . 7  setvar  z
76cv 1361 . . . . . 6  class  z
8 clt 9406 . . . . . 6  class  <
95, 7, 8wbr 4280 . . . . 5  wff  x  < 
z
103cv 1361 . . . . . 6  class  y
11 cle 9407 . . . . . 6  class  <_
127, 10, 11wbr 4280 . . . . 5  wff  z  <_ 
y
139, 12wa 369 . . . 4  wff  ( x  <  z  /\  z  <_  y )
1413, 6, 4crab 2709 . . 3  class  { z  e.  RR*  |  (
x  <  z  /\  z  <_  y ) }
152, 3, 4, 4, 14cmpt2 6082 . 2  class  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <  z  /\  z  <_ 
y ) } )
161, 15wceq 1362 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  11325  elioc1  11330  iocssxr  11367  snunioc  11400  leordtval2  18658  iocpnfordt  18661  lecldbas  18665  pnfnei  18666  iocmnfcld  20190  xrtgioo  20225  ismbf3d  20974  dvloglem  21978  iocssicc  25882  iocssioo  25884  asindmre  28323  dvasin  28324  ioounsn  29430
  Copyright terms: Public domain W3C validator