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

Definition df-icc 11667
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 11663 . 2  class  [,]
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 cxr 9692 . . 3  class  RR*
52cv 1451 . . . . . 6  class  x
6 vz . . . . . . 7  setvar  z
76cv 1451 . . . . . 6  class  z
8 cle 9694 . . . . . 6  class  <_
95, 7, 8wbr 4395 . . . . 5  wff  x  <_ 
z
103cv 1451 . . . . . 6  class  y
117, 10, 8wbr 4395 . . . . 5  wff  z  <_ 
y
129, 11wa 376 . . . 4  wff  ( x  <_  z  /\  z  <_  y )
1312, 6, 4crab 2760 . . 3  class  { z  e.  RR*  |  (
x  <_  z  /\  z  <_  y ) }
142, 3, 4, 4, 13cmpt2 6310 . 2  class  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <_  z  /\  z  <_ 
y ) } )
151, 14wceq 1452 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  11700  elicc1  11705  iccss  11727  iccssioo  11728  iccss2  11730  iccssico  11731  iccssxr  11742  ioossicc  11745  icossicc  11746  iocssicc  11747  iccf  11758  snunioo  11784  snunico  11785  snunioc  11786  ioodisj  11788  leordtval2  20305  iccordt  20307  lecldbas  20312  ioombl  22597  itgspliticc  22873  psercnlem2  23458  tanord1  23565  cvmliftlem10  30089  ftc1anclem7  32087  ftc1anclem8  32088  ftc1anc  32089  ioounsn  36165  snunioo2  37702  snunioo1  37709
  Copyright terms: Public domain W3C validator