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

Definition df-icc 11546
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 11542 . 2  class  [,]
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 cxr 9630 . . 3  class  RR*
52cv 1382 . . . . . 6  class  x
6 vz . . . . . . 7  setvar  z
76cv 1382 . . . . . 6  class  z
8 cle 9632 . . . . . 6  class  <_
95, 7, 8wbr 4437 . . . . 5  wff  x  <_ 
z
103cv 1382 . . . . . 6  class  y
117, 10, 8wbr 4437 . . . . 5  wff  z  <_ 
y
129, 11wa 369 . . . 4  wff  ( x  <_  z  /\  z  <_  y )
1312, 6, 4crab 2797 . . 3  class  { z  e.  RR*  |  (
x  <_  z  /\  z  <_  y ) }
142, 3, 4, 4, 13cmpt2 6283 . 2  class  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <_  z  /\  z  <_ 
y ) } )
151, 14wceq 1383 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  11578  elicc1  11583  iccss  11602  iccssioo  11603  iccss2  11605  iccssico  11606  iccssxr  11617  ioossicc  11620  icossicc  11621  iocssicc  11622  iccf  11633  snunioo  11656  snunico  11657  snunioc  11658  ioodisj  11660  leordtval2  19690  iccordt  19692  lecldbas  19697  ioombl  21952  itgspliticc  22220  psercnlem2  22795  tanord1  22900  cvmliftlem10  28716  ftc1anclem7  30071  ftc1anclem8  30072  ftc1anc  30073  ioounsn  31153  snunioo2  31480  snunioo1  31488
  Copyright terms: Public domain W3C validator