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

Definition df-icc 10663
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 10659 . 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 cle 8868 . . . . . 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:  iccval  10695  elicc1  10700  iccss  10718  iccssioo  10719  iccss2  10720  iccssico  10721  iccssxr  10732  ioossicc  10735  iccf  10742  snunioo  10762  snunico  10763  ioodisj  10765  leordtval2  16942  iccordt  16944  lecldbas  16949  ioombl  18922  itg2mulclem  19101  itg2mulc  19102  itgspliticc  19191  psercnlem2  19800  tanord1  19899  icossicc  23258  iocssicc  23259  snunioc  23267  cvmliftlem10  23825
  Copyright terms: Public domain W3C validator