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

Definition df-ioo 10660
Description: Define the set of open intervals of extended reals. (Contributed by NM, 24-Dec-2006.)
Assertion
Ref Expression
df-ioo  |-  (,)  =  ( 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-ioo
StepHypRef Expression
1 cioo 10656 . 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
117, 10, 8wbr 4023 . . . . 5  wff  z  < 
y
129, 11wa 358 . . . 4  wff  ( x  <  z  /\  z  <  y )
1312, 6, 4crab 2547 . . 3  class  { z  e.  RR*  |  (
x  <  z  /\  z  <  y ) }
142, 3, 4, 4, 13cmpt2 5860 . 2  class  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <  z  /\  z  < 
y ) } )
151, 14wceq 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:  iooex  10679  iooval  10680  ndmioo  10683  elioo3g  10685  iooin  10690  iooss1  10691  iooss2  10692  elioo1  10696  iccssioo  10719  ioossicc  10735  ioof  10741  snunioo  10762  ioodisj  10765  ioojoin  10766  ioopnfsup  10968  leordtval  16943  icopnfcld  18277  iocmnfcld  18278  bndth  18456  ioombl  18922  ioorf  18928  ioorinv2  18930  ismbf3d  19009  dvfsumrlimge0  19377  dvfsumrlim2  19379  tanord1  19899  dvloglem  19995  rlimcnp  20260  rlimcnp2  20261  dchrisum0lem2a  20666  pnt  20763  ioossico  23260  iocssioo  23261  icossioo  23262  ioossioo  23264  joiniooico  23265
  Copyright terms: Public domain W3C validator