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

Definition df-ioc 11640
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 11636 . 2  class  (,]
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 cxr 9673 . . 3  class  RR*
52cv 1436 . . . . . 6  class  x
6 vz . . . . . . 7  setvar  z
76cv 1436 . . . . . 6  class  z
8 clt 9674 . . . . . 6  class  <
95, 7, 8wbr 4426 . . . . 5  wff  x  < 
z
103cv 1436 . . . . . 6  class  y
11 cle 9675 . . . . . 6  class  <_
127, 10, 11wbr 4426 . . . . 5  wff  z  <_ 
y
139, 12wa 370 . . . 4  wff  ( x  <  z  /\  z  <_  y )
1413, 6, 4crab 2786 . . 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  11673  elioc1  11678  iocssxr  11718  iocssicc  11722  iocssioo  11724  snunioc  11758  leordtval2  20159  iocpnfordt  20162  lecldbas  20166  pnfnei  20167  iocmnfcld  21700  xrtgioo  21735  ismbf3d  22487  dvloglem  23458  asindmre  31730  dvasin  31731  ioounsn  35792  ioossioc  37172  snunioo2  37190  eliocre  37193  lbioc  37198
  Copyright terms: Public domain W3C validator