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

Definition df-icc 10879
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 10875 . 2  class  [,]
2 vx . . 3  set  x
3 vy . . 3  set  y
4 cxr 9075 . . 3  class  RR*
52cv 1648 . . . . . 6  class  x
6 vz . . . . . . 7  set  z
76cv 1648 . . . . . 6  class  z
8 cle 9077 . . . . . 6  class  <_
95, 7, 8wbr 4172 . . . . 5  wff  x  <_ 
z
103cv 1648 . . . . . 6  class  y
117, 10, 8wbr 4172 . . . . 5  wff  z  <_ 
y
129, 11wa 359 . . . 4  wff  ( x  <_  z  /\  z  <_  y )
1312, 6, 4crab 2670 . . 3  class  { z  e.  RR*  |  (
x  <_  z  /\  z  <_  y ) }
142, 3, 4, 4, 13cmpt2 6042 . 2  class  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <_  z  /\  z  <_ 
y ) } )
151, 14wceq 1649 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  10911  elicc1  10916  iccss  10934  iccssioo  10935  iccss2  10937  iccssico  10938  iccssxr  10949  ioossicc  10952  iccf  10959  snunioo  10979  snunico  10980  ioodisj  10982  leordtval2  17230  iccordt  17232  lecldbas  17237  ioombl  19412  itg2mulclem  19591  itg2mulc  19592  itgspliticc  19681  psercnlem2  20293  tanord1  20392  icossicc  24082  iocssicc  24083  snunioc  24090  cvmliftlem10  24934
  Copyright terms: Public domain W3C validator