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

Definition df-icc 11295
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 11291 . 2  class  [,]
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 cxr 9405 . . 3  class  RR*
52cv 1361 . . . . . 6  class  x
6 vz . . . . . . 7  setvar  z
76cv 1361 . . . . . 6  class  z
8 cle 9407 . . . . . 6  class  <_
95, 7, 8wbr 4280 . . . . 5  wff  x  <_ 
z
103cv 1361 . . . . . 6  class  y
117, 10, 8wbr 4280 . . . . 5  wff  z  <_ 
y
129, 11wa 369 . . . 4  wff  ( x  <_  z  /\  z  <_  y )
1312, 6, 4crab 2709 . . 3  class  { z  e.  RR*  |  (
x  <_  z  /\  z  <_  y ) }
142, 3, 4, 4, 13cmpt2 6082 . 2  class  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <_  z  /\  z  <_ 
y ) } )
151, 14wceq 1362 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  11327  elicc1  11332  iccss  11351  iccssioo  11352  iccss2  11354  iccssico  11355  iccssxr  11366  ioossicc  11369  iccf  11376  snunioo  11398  snunico  11399  snunioc  11400  ioodisj  11402  leordtval2  18658  iccordt  18660  lecldbas  18665  ioombl  20888  itg2mulclem  21066  itg2mulc  21067  itgspliticc  21156  psercnlem2  21774  tanord1  21878  icossicc  25881  iocssicc  25882  cvmliftlem10  27031  ftc1anclem7  28317  ftc1anclem8  28318  ftc1anc  28319  ioounsn  29430
  Copyright terms: Public domain W3C validator