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

Definition df-icc 11268
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 11264 . 2  class  [,]
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 cxr 9378 . . 3  class  RR*
52cv 1353 . . . . . 6  class  x
6 vz . . . . . . 7  setvar  z
76cv 1353 . . . . . 6  class  z
8 cle 9380 . . . . . 6  class  <_
95, 7, 8wbr 4271 . . . . 5  wff  x  <_ 
z
103cv 1353 . . . . . 6  class  y
117, 10, 8wbr 4271 . . . . 5  wff  z  <_ 
y
129, 11wa 362 . . . 4  wff  ( x  <_  z  /\  z  <_  y )
1312, 6, 4crab 2702 . . 3  class  { z  e.  RR*  |  (
x  <_  z  /\  z  <_  y ) }
142, 3, 4, 4, 13cmpt2 6067 . 2  class  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <_  z  /\  z  <_ 
y ) } )
151, 14wceq 1354 1  wff  [,]  =  ( x  e.  RR* ,  y  e.  RR*  |->  { z  e.  RR*  |  (
x  <_  z  /\  z  <_  y ) } )
Colors of variables: wff setvar class
This definition is referenced by:  iccval  11300  elicc1  11305  iccss  11324  iccssioo  11325  iccss2  11327  iccssico  11328  iccssxr  11339  ioossicc  11342  iccf  11349  snunioo  11371  snunico  11372  snunioc  11373  ioodisj  11375  leordtval2  18610  iccordt  18612  lecldbas  18617  ioombl  20836  itg2mulclem  21014  itg2mulc  21015  itgspliticc  21104  psercnlem2  21720  tanord1  21824  icossicc  25826  iocssicc  25827  cvmliftlem10  26976  ftc1anclem7  28234  ftc1anclem8  28235  ftc1anc  28236  ioounsn  29348
  Copyright terms: Public domain W3C validator