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

Definition df-ioo 10909
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 10905 . 2  class  (,)
2 vx . . 3  set  x
3 vy . . 3  set  y
4 cxr 9108 . . 3  class  RR*
52cv 1651 . . . . . 6  class  x
6 vz . . . . . . 7  set  z
76cv 1651 . . . . . 6  class  z
8 clt 9109 . . . . . 6  class  <
95, 7, 8wbr 4204 . . . . 5  wff  x  < 
z
103cv 1651 . . . . . 6  class  y
117, 10, 8wbr 4204 . . . . 5  wff  z  < 
y
129, 11wa 359 . . . 4  wff  ( x  <  z  /\  z  <  y )
1312, 6, 4crab 2701 . . 3  class  { z  e.  RR*  |  (
x  <  z  /\  z  <  y ) }
142, 3, 4, 4, 13cmpt2 6074 . 2  class  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <  z  /\  z  < 
y ) } )
151, 14wceq 1652 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  10928  iooval  10929  ndmioo  10932  elioo3g  10934  iooin  10939  iooss1  10940  iooss2  10941  elioo1  10945  iccssioo  10968  ioossicc  10985  ioof  10991  snunioo  11012  ioodisj  11015  ioojoin  11016  ioopnfsup  11233  leordtval  17265  icopnfcld  18790  iocmnfcld  18791  bndth  18971  ioombl  19447  ioorf  19453  ioorinv2  19455  ismbf3d  19534  dvfsumrlimge0  19902  dvfsumrlim2  19904  tanord1  20427  dvloglem  20527  rlimcnp  20792  rlimcnp2  20793  dchrisum0lem2a  21199  pnt  21296  ioossico  24119  iocssioo  24120  icossioo  24121  ioossioo  24122  joiniooico  24123  tpr2rico  24298  ftc1cnnclem  26224
  Copyright terms: Public domain W3C validator