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

Definition df-ioc 11545
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 11541 . 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 clt 9631 . . . . . 6  class  <
95, 7, 8wbr 4437 . . . . 5  wff  x  < 
z
103cv 1382 . . . . . 6  class  y
11 cle 9632 . . . . . 6  class  <_
127, 10, 11wbr 4437 . . . . 5  wff  z  <_ 
y
139, 12wa 369 . . . 4  wff  ( x  <  z  /\  z  <_  y )
1413, 6, 4crab 2797 . . 3  class  { z  e.  RR*  |  (
x  <  z  /\  z  <_  y ) }
152, 3, 4, 4, 14cmpt2 6283 . 2  class  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <  z  /\  z  <_ 
y ) } )
161, 15wceq 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:  iocval  11577  elioc1  11582  iocssxr  11619  iocssicc  11623  iocssioo  11625  snunioc  11659  leordtval2  19691  iocpnfordt  19694  lecldbas  19698  pnfnei  19699  iocmnfcld  21254  xrtgioo  21289  ismbf3d  22039  dvloglem  23007  asindmre  30078  dvasin  30079  ioounsn  31153  ioossioc  31478  snunioo2  31498  eliocre  31501  lbioc  31507
  Copyright terms: Public domain W3C validator