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

Definition df-ioc 11630
Description: Define the set of open-below, closed-above intervals of extended reals. (Contributed by NM, 24-Dec-2006.)
Assertion
Ref Expression
df-ioc  |-  (,]  =  ( 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-ioc
StepHypRef Expression
1 cioc 11626 . 2  class  (,]
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 cxr 9661 . . 3  class  RR*
52cv 1447 . . . . . 6  class  x
6 vz . . . . . . 7  setvar  z
76cv 1447 . . . . . 6  class  z
8 clt 9662 . . . . . 6  class  <
95, 7, 8wbr 4374 . . . . 5  wff  x  < 
z
103cv 1447 . . . . . 6  class  y
11 cle 9663 . . . . . 6  class  <_
127, 10, 11wbr 4374 . . . . 5  wff  z  <_ 
y
139, 12wa 375 . . . 4  wff  ( x  <  z  /\  z  <_  y )
1413, 6, 4crab 2741 . . 3  class  { z  e.  RR*  |  (
x  <  z  /\  z  <_  y ) }
152, 3, 4, 4, 14cmpt2 6278 . 2  class  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <  z  /\  z  <_ 
y ) } )
161, 15wceq 1448 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:  iocval  11663  elioc1  11668  iocssxr  11708  iocssicc  11712  iocssioo  11714  snunioc  11751  leordtval2  20239  iocpnfordt  20242  lecldbas  20246  pnfnei  20247  iocmnfcld  21800  xrtgioo  21835  ismbf3d  22622  dvloglem  23605  asindmre  32029  dvasin  32030  ioounsn  36096  ioossioc  37629  snunioo2  37647  eliocre  37650  lbioc  37655
  Copyright terms: Public domain W3C validator