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

Definition df-ioc 11530
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 11526 . 2  class  (,]
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 cxr 9623 . . 3  class  RR*
52cv 1378 . . . . . 6  class  x
6 vz . . . . . . 7  setvar  z
76cv 1378 . . . . . 6  class  z
8 clt 9624 . . . . . 6  class  <
95, 7, 8wbr 4447 . . . . 5  wff  x  < 
z
103cv 1378 . . . . . 6  class  y
11 cle 9625 . . . . . 6  class  <_
127, 10, 11wbr 4447 . . . . 5  wff  z  <_ 
y
139, 12wa 369 . . . 4  wff  ( x  <  z  /\  z  <_  y )
1413, 6, 4crab 2818 . . 3  class  { z  e.  RR*  |  (
x  <  z  /\  z  <_  y ) }
152, 3, 4, 4, 14cmpt2 6284 . 2  class  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <  z  /\  z  <_ 
y ) } )
161, 15wceq 1379 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  11562  elioc1  11567  iocssxr  11604  iocssicc  11608  iocssioo  11610  snunioc  11644  leordtval2  19476  iocpnfordt  19479  lecldbas  19483  pnfnei  19484  iocmnfcld  21008  xrtgioo  21043  ismbf3d  21793  dvloglem  22754  asindmre  29677  dvasin  29678  ioounsn  30782  ioossioc  31088  snunioo2  31108  eliocre  31111  lbioc  31117
  Copyright terms: Public domain W3C validator