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

Definition df-icc 11644
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 11640 . 2  class  [,]
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 cxr 9676 . . 3  class  RR*
52cv 1437 . . . . . 6  class  x
6 vz . . . . . . 7  setvar  z
76cv 1437 . . . . . 6  class  z
8 cle 9678 . . . . . 6  class  <_
95, 7, 8wbr 4421 . . . . 5  wff  x  <_ 
z
103cv 1437 . . . . . 6  class  y
117, 10, 8wbr 4421 . . . . 5  wff  z  <_ 
y
129, 11wa 371 . . . 4  wff  ( x  <_  z  /\  z  <_  y )
1312, 6, 4crab 2780 . . 3  class  { z  e.  RR*  |  (
x  <_  z  /\  z  <_  y ) }
142, 3, 4, 4, 13cmpt2 6305 . 2  class  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <_  z  /\  z  <_ 
y ) } )
151, 14wceq 1438 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  11677  elicc1  11682  iccss  11704  iccssioo  11705  iccss2  11707  iccssico  11708  iccssxr  11719  ioossicc  11722  icossicc  11723  iocssicc  11724  iccf  11735  snunioo  11760  snunico  11761  snunioc  11762  ioodisj  11764  leordtval2  20220  iccordt  20222  lecldbas  20227  ioombl  22510  itgspliticc  22786  psercnlem2  23371  tanord1  23478  cvmliftlem10  30019  ftc1anclem7  31981  ftc1anclem8  31982  ftc1anc  31983  ioounsn  36058  snunioo2  37481  snunioo1  37488
  Copyright terms: Public domain W3C validator