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

Definition df-icc 11299
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 11295 . 2  class  [,]
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 cxr 9409 . . 3  class  RR*
52cv 1368 . . . . . 6  class  x
6 vz . . . . . . 7  setvar  z
76cv 1368 . . . . . 6  class  z
8 cle 9411 . . . . . 6  class  <_
95, 7, 8wbr 4287 . . . . 5  wff  x  <_ 
z
103cv 1368 . . . . . 6  class  y
117, 10, 8wbr 4287 . . . . 5  wff  z  <_ 
y
129, 11wa 369 . . . 4  wff  ( x  <_  z  /\  z  <_  y )
1312, 6, 4crab 2714 . . 3  class  { z  e.  RR*  |  (
x  <_  z  /\  z  <_  y ) }
142, 3, 4, 4, 13cmpt2 6088 . 2  class  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <_  z  /\  z  <_ 
y ) } )
151, 14wceq 1369 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  11331  elicc1  11336  iccss  11355  iccssioo  11356  iccss2  11358  iccssico  11359  iccssxr  11370  ioossicc  11373  iccf  11380  snunioo  11403  snunico  11404  snunioc  11405  ioodisj  11407  leordtval2  18791  iccordt  18793  lecldbas  18798  ioombl  21021  itg2mulclem  21199  itg2mulc  21200  itgspliticc  21289  psercnlem2  21864  tanord1  21968  icossicc  26009  iocssicc  26010  cvmliftlem10  27135  ftc1anclem7  28426  ftc1anclem8  28427  ftc1anc  28428  ioounsn  29538
  Copyright terms: Public domain W3C validator