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 12219
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 12215 . 2 class [,)
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cxr 10111 . . 3 class *
52cv 1522 . . . . . 6 class 𝑥
6 vz . . . . . . 7 setvar 𝑧
76cv 1522 . . . . . 6 class 𝑧
8 cle 10113 . . . . . 6 class
95, 7, 8wbr 4685 . . . . 5 wff 𝑥𝑧
103cv 1522 . . . . . 6 class 𝑦
11 clt 10112 . . . . . 6 class <
127, 10, 11wbr 4685 . . . . 5 wff 𝑧 < 𝑦
139, 12wa 383 . . . 4 wff (𝑥𝑧𝑧 < 𝑦)
1413, 6, 4crab 2945 . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧 < 𝑦)}
152, 3, 4, 4, 14cmpt2 6692 . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧 < 𝑦)})
161, 15wceq 1523 1 wff [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧 < 𝑦)})
Colors of variables: wff setvar class
This definition is referenced by:  icoval  12251  elico1  12256  elicore  12264  icossico  12281  iccssico  12283  iccssico2  12285  icossxr  12296  icossicc  12298  ioossico  12300  icossioo  12302  icoun  12334  snunioo  12336  snunico  12337  ioojoin  12341  icopnfsup  12704  limsupgord  14247  leordtval2  21064  icomnfordt  21068  lecldbas  21071  mnfnei  21073  icopnfcld  22618  xrtgioo  22656  ioombl  23379  dvfsumrlimge0  23838  dvfsumrlim2  23840  psercnlem2  24223  tanord1  24328  rlimcnp  24737  rlimcnp2  24738  dchrisum0lem2a  25251  pntleml  25345  pnt  25348  joiniooico  29664  icorempt2  33329  icoreresf  33330  isbasisrelowl  33336  icoreelrn  33339  relowlpssretop  33342  asindmre  33625  icof  39725  snunioo1  40056  elicores  40078  dmico  40110  liminfgord  40304  volicorescl  41088
  Copyright terms: Public domain W3C validator