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

Definition df-ico 11564
Description: Define the set of closed-below, open-above intervals of extended reals. (Contributed by NM, 24-Dec-2006.)
Assertion
Ref Expression
df-ico
Distinct variable group:   , ,

Detailed syntax breakdown of Definition df-ico
StepHypRef Expression
1 cico 11560 . 2
2 vx . . 3
3 vy . . 3
4 cxr 9648 . . 3
52cv 1394 . . . . . 6
6 vz . . . . . . 7
76cv 1394 . . . . . 6
8 cle 9650 . . . . . 6
95, 7, 8wbr 4452 . . . . 5
103cv 1394 . . . . . 6
11 clt 9649 . . . . . 6
127, 10, 11wbr 4452 . . . . 5
139, 12wa 369 . . . 4
1413, 6, 4crab 2811 . . 3
152, 3, 4, 4, 14cmpt2 6298 . 2
161, 15wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  icoval  11596  elico1  11601  icossico  11623  iccssico  11625  iccssico2  11627  icossxr  11638  icossicc  11640  ioossico  11642  icossioo  11644  icoun  11673  snunioo  11675  snunico  11676  ioojoin  11680  icopnfsup  11992  limsupgord  13295  leordtval2  19713  icomnfordt  19717  lecldbas  19720  mnfnei  19722  icopnfcld  21275  xrtgioo  21311  ioombl  21975  dvfsumrlimge0  22431  dvfsumrlim2  22433  psercnlem2  22819  tanord1  22924  rlimcnp  23295  rlimcnp2  23296  dchrisum0lem2a  23702  pntleml  23796  pnt  23799  joiniooico  27585  asindmre  30102  elicore  31537  snunioo1  31552
  Copyright terms: Public domain W3C validator