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

Definition df-ioc 10661
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 10657 . 2  class  (,]
2 vx . . 3  set  x
3 vy . . 3  set  y
4 cxr 8866 . . 3  class  RR*
52cv 1622 . . . . . 6  class  x
6 vz . . . . . . 7  set  z
76cv 1622 . . . . . 6  class  z
8 clt 8867 . . . . . 6  class  <
95, 7, 8wbr 4023 . . . . 5  wff  x  < 
z
103cv 1622 . . . . . 6  class  y
11 cle 8868 . . . . . 6  class  <_
127, 10, 11wbr 4023 . . . . 5  wff  z  <_ 
y
139, 12wa 358 . . . 4  wff  ( x  <  z  /\  z  <_  y )
1413, 6, 4crab 2547 . . 3  class  { z  e.  RR*  |  (
x  <  z  /\  z  <_  y ) }
152, 3, 4, 4, 14cmpt2 5860 . 2  class  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <  z  /\  z  <_ 
y ) } )
161, 15wceq 1623 1  wff  (,]  =  ( x  e.  RR* ,  y  e.  RR*  |->  { z  e.  RR*  |  (
x  <  z  /\  z  <_  y ) } )
Colors of variables: wff set class
This definition is referenced by:  iocval  10693  elioc1  10698  iocssxr  10733  leordtval2  16942  iocpnfordt  16945  lecldbas  16949  pnfnei  16950  iocmnfcld  18278  xrtgioo  18312  ismbf3d  19009  dvloglem  19995  iocssicc  23259  iocssioo  23261  snunioc  23267  iocf  25642
  Copyright terms: Public domain W3C validator