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

Definition df-icc 10923
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 10919 . 2  class  [,]
2 vx . . 3  set  x
3 vy . . 3  set  y
4 cxr 9119 . . 3  class  RR*
52cv 1651 . . . . . 6  class  x
6 vz . . . . . . 7  set  z
76cv 1651 . . . . . 6  class  z
8 cle 9121 . . . . . 6  class  <_
95, 7, 8wbr 4212 . . . . 5  wff  x  <_ 
z
103cv 1651 . . . . . 6  class  y
117, 10, 8wbr 4212 . . . . 5  wff  z  <_ 
y
129, 11wa 359 . . . 4  wff  ( x  <_  z  /\  z  <_  y )
1312, 6, 4crab 2709 . . 3  class  { z  e.  RR*  |  (
x  <_  z  /\  z  <_  y ) }
142, 3, 4, 4, 13cmpt2 6083 . 2  class  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <_  z  /\  z  <_ 
y ) } )
151, 14wceq 1652 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  10955  elicc1  10960  iccss  10978  iccssioo  10979  iccss2  10981  iccssico  10982  iccssxr  10993  ioossicc  10996  iccf  11003  snunioo  11023  snunico  11024  ioodisj  11026  leordtval2  17276  iccordt  17278  lecldbas  17283  ioombl  19459  itg2mulclem  19638  itg2mulc  19639  itgspliticc  19728  psercnlem2  20340  tanord1  20439  icossicc  24129  iocssicc  24130  snunioc  24137  cvmliftlem10  24981  ftc1anclem7  26286  ftc1anclem8  26287  ftc1anc  26288
  Copyright terms: Public domain W3C validator