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

Definition df-ioc 11297
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 11293 . 2  class  (,]
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 cxr 9409 . . 3  class  RR*
52cv 1368 . . . . . 6  class  x
6 vz . . . . . . 7  setvar  z
76cv 1368 . . . . . 6  class  z
8 clt 9410 . . . . . 6  class  <
95, 7, 8wbr 4287 . . . . 5  wff  x  < 
z
103cv 1368 . . . . . 6  class  y
11 cle 9411 . . . . . 6  class  <_
127, 10, 11wbr 4287 . . . . 5  wff  z  <_ 
y
139, 12wa 369 . . . 4  wff  ( x  <  z  /\  z  <_  y )
1413, 6, 4crab 2714 . . 3  class  { z  e.  RR*  |  (
x  <  z  /\  z  <_  y ) }
152, 3, 4, 4, 14cmpt2 6088 . 2  class  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <  z  /\  z  <_ 
y ) } )
161, 15wceq 1369 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  11329  elioc1  11334  iocssxr  11371  snunioc  11405  leordtval2  18791  iocpnfordt  18794  lecldbas  18798  pnfnei  18799  iocmnfcld  20323  xrtgioo  20358  ismbf3d  21107  dvloglem  22068  iocssicc  26010  iocssioo  26012  asindmre  28432  dvasin  28433  ioounsn  29538
  Copyright terms: Public domain W3C validator