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

Definition df-ioc 10677
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 10673 . 2  class  (,]
2 vx . . 3  set  x
3 vy . . 3  set  y
4 cxr 8882 . . 3  class  RR*
52cv 1631 . . . . . 6  class  x
6 vz . . . . . . 7  set  z
76cv 1631 . . . . . 6  class  z
8 clt 8883 . . . . . 6  class  <
95, 7, 8wbr 4039 . . . . 5  wff  x  < 
z
103cv 1631 . . . . . 6  class  y
11 cle 8884 . . . . . 6  class  <_
127, 10, 11wbr 4039 . . . . 5  wff  z  <_ 
y
139, 12wa 358 . . . 4  wff  ( x  <  z  /\  z  <_  y )
1413, 6, 4crab 2560 . . 3  class  { z  e.  RR*  |  (
x  <  z  /\  z  <_  y ) }
152, 3, 4, 4, 14cmpt2 5876 . 2  class  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <  z  /\  z  <_ 
y ) } )
161, 15wceq 1632 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  10709  elioc1  10714  iocssxr  10749  leordtval2  16958  iocpnfordt  16961  lecldbas  16965  pnfnei  16966  iocmnfcld  18294  xrtgioo  18328  ismbf3d  19025  dvloglem  20011  iocssicc  23274  iocssioo  23276  snunioc  23282  iocf  25745
  Copyright terms: Public domain W3C validator