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

Definition df-icc 10658
Description: Define the set of closed intervals of extended reals. (Contributed by NM, 24-Dec-2006.)
Assertion
Ref Expression
df-icc  |-  [,]  =  ( 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-icc
StepHypRef Expression
1 cicc 10654 . 2  class  [,]
2 vx . . 3  set  x
3 vy . . 3  set  y
4 cxr 8862 . . 3  class  RR*
52cv 1623 . . . . . 6  class  x
6 vz . . . . . . 7  set  z
76cv 1623 . . . . . 6  class  z
8 cle 8864 . . . . . 6  class  <_
95, 7, 8wbr 4025 . . . . 5  wff  x  <_ 
z
103cv 1623 . . . . . 6  class  y
117, 10, 8wbr 4025 . . . . 5  wff  z  <_ 
y
129, 11wa 360 . . . 4  wff  ( x  <_  z  /\  z  <_  y )
1312, 6, 4crab 2549 . . 3  class  { z  e.  RR*  |  (
x  <_  z  /\  z  <_  y ) }
142, 3, 4, 4, 13cmpt2 5822 . 2  class  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <_  z  /\  z  <_ 
y ) } )
151, 14wceq 1624 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:  iccval  10690  elicc1  10695  iccss  10713  iccssioo  10714  iccss2  10715  iccssico  10716  iccssxr  10727  ioossicc  10730  iccf  10737  snunioo  10757  snunico  10758  ioodisj  10760  leordtval2  16937  iccordt  16939  lecldbas  16944  ioombl  18917  itg2mulclem  19096  itg2mulc  19097  itgspliticc  19186  psercnlem2  19795  tanord1  19894  cvmliftlem10  23230
  Copyright terms: Public domain W3C validator