ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-ioo Unicode version

Definition df-ioo 9892
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 9888 . 2  class  (,)
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 cxr 7991 . . 3  class  RR*
52cv 1352 . . . . . 6  class  x
6 vz . . . . . . 7  setvar  z
76cv 1352 . . . . . 6  class  z
8 clt 7992 . . . . . 6  class  <
95, 7, 8wbr 4004 . . . . 5  wff  x  < 
z
103cv 1352 . . . . . 6  class  y
117, 10, 8wbr 4004 . . . . 5  wff  z  < 
y
129, 11wa 104 . . . 4  wff  ( x  <  z  /\  z  <  y )
1312, 6, 4crab 2459 . . 3  class  { z  e.  RR*  |  (
x  <  z  /\  z  <  y ) }
142, 3, 4, 4, 13cmpo 5877 . 2  class  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <  z  /\  z  < 
y ) } )
151, 14wceq 1353 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  9907  iooval  9908  elioo3g  9910  elioo1  9911  iooss1  9916  iooss2  9917  eliooxr  9927  iccssioo  9942  ioossicc  9959  ioossico  9962  iocssioo  9963  icossioo  9964  ioossioo  9965  ioof  9971  ioodisj  9993
  Copyright terms: Public domain W3C validator