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

Definition df-ico 8982
Description: Define the set of closed-below, open-above intervals of extended reals. (Contributed by NM, 24-Dec-2006.)
Assertion
Ref Expression
df-ico  |-  [,)  =  ( 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-ico
StepHypRef Expression
1 cico 8978 . 2  class  [,)
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 cxr 7203 . . 3  class  RR*
52cv 1284 . . . . . 6  class  x
6 vz . . . . . . 7  setvar  z
76cv 1284 . . . . . 6  class  z
8 cle 7205 . . . . . 6  class  <_
95, 7, 8wbr 3787 . . . . 5  wff  x  <_ 
z
103cv 1284 . . . . . 6  class  y
11 clt 7204 . . . . . 6  class  <
127, 10, 11wbr 3787 . . . . 5  wff  z  < 
y
139, 12wa 102 . . . 4  wff  ( x  <_  z  /\  z  <  y )
1413, 6, 4crab 2353 . . 3  class  { z  e.  RR*  |  (
x  <_  z  /\  z  <  y ) }
152, 3, 4, 4, 14cmpt2 5539 . 2  class  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <_  z  /\  z  < 
y ) } )
161, 15wceq 1285 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:  icoval  9007  elico1  9011  icossico  9031  iccssico  9033  iccssico2  9035  icossxr  9046  icossicc  9048  ioossico  9050  icossioo  9052
  Copyright terms: Public domain W3C validator