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

Definition df-icc 11535
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 11531 . 2  class  [,]
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 cxr 9626 . . 3  class  RR*
52cv 1378 . . . . . 6  class  x
6 vz . . . . . . 7  setvar  z
76cv 1378 . . . . . 6  class  z
8 cle 9628 . . . . . 6  class  <_
95, 7, 8wbr 4447 . . . . 5  wff  x  <_ 
z
103cv 1378 . . . . . 6  class  y
117, 10, 8wbr 4447 . . . . 5  wff  z  <_ 
y
129, 11wa 369 . . . 4  wff  ( x  <_  z  /\  z  <_  y )
1312, 6, 4crab 2818 . . 3  class  { z  e.  RR*  |  (
x  <_  z  /\  z  <_  y ) }
142, 3, 4, 4, 13cmpt2 6285 . 2  class  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <_  z  /\  z  <_ 
y ) } )
151, 14wceq 1379 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  11567  elicc1  11572  iccss  11591  iccssioo  11592  iccss2  11594  iccssico  11595  iccssxr  11606  ioossicc  11609  icossicc  11610  iocssicc  11611  iccf  11622  snunioo  11645  snunico  11646  snunioc  11647  ioodisj  11649  leordtval2  19495  iccordt  19497  lecldbas  19502  ioombl  21726  itg2mulclem  21904  itg2mulc  21905  itgspliticc  21994  psercnlem2  22569  tanord1  22673  cvmliftlem10  28395  ftc1anclem7  29689  ftc1anclem8  29690  ftc1anc  29691  ioounsn  30798  snunioo2  31124  snunioo1  31132
  Copyright terms: Public domain W3C validator