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

Definition df-ico 12734
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 12730 . 2 class [,)
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cxr 10663 . . 3 class *
52cv 1527 . . . . . 6 class 𝑥
6 vz . . . . . . 7 setvar 𝑧
76cv 1527 . . . . . 6 class 𝑧
8 cle 10665 . . . . . 6 class
95, 7, 8wbr 5058 . . . . 5 wff 𝑥𝑧
103cv 1527 . . . . . 6 class 𝑦
11 clt 10664 . . . . . 6 class <
127, 10, 11wbr 5058 . . . . 5 wff 𝑧 < 𝑦
139, 12wa 396 . . . 4 wff (𝑥𝑧𝑧 < 𝑦)
1413, 6, 4crab 3142 . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧 < 𝑦)}
152, 3, 4, 4, 14cmpo 7147 . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧 < 𝑦)})
161, 15wceq 1528 1 wff [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧 < 𝑦)})
Colors of variables: wff setvar class
This definition is referenced by:  icoval  12766  elico1  12771  elicore  12779  icossico  12796  iccssico  12798  iccssico2  12800  icossxr  12811  icossicc  12814  ioossico  12816  icossioo  12818  icoun  12851  snunioo  12854  snunico  12855  ioojoin  12859  icopnfsup  13223  limsupgord  14819  leordtval2  21750  icomnfordt  21754  lecldbas  21757  mnfnei  21759  icopnfcld  23305  xrtgioo  23343  ioombl  24095  dvfsumrlimge0  24556  dvfsumrlim2  24558  psercnlem2  24941  tanord1  25048  rlimcnp  25471  rlimcnp2  25472  dchrisum0lem2a  26021  pntleml  26115  pnt  26118  joiniooico  30424  icorempo  34515  icoreresf  34516  isbasisrelowl  34522  icoreelrn  34525  relowlpssretop  34528  asindmre  34859  icof  41362  snunioo1  41668  elicores  41689  dmico  41721  liminfgord  41915  volicorescl  42716
  Copyright terms: Public domain W3C validator