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

Definition df-icc 12403
Description: Define the set of closed intervals of extended reals. (Contributed by NM, 24-Dec-2006.)
Assertion
Ref Expression
df-icc [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧𝑦)})
Distinct variable group:   𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-icc
StepHypRef Expression
1 cicc 12399 . 2 class [,]
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cxr 10361 . . 3 class *
52cv 1636 . . . . . 6 class 𝑥
6 vz . . . . . . 7 setvar 𝑧
76cv 1636 . . . . . 6 class 𝑧
8 cle 10363 . . . . . 6 class
95, 7, 8wbr 4851 . . . . 5 wff 𝑥𝑧
103cv 1636 . . . . . 6 class 𝑦
117, 10, 8wbr 4851 . . . . 5 wff 𝑧𝑦
129, 11wa 384 . . . 4 wff (𝑥𝑧𝑧𝑦)
1312, 6, 4crab 3107 . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧𝑦)}
142, 3, 4, 4, 13cmpt2 6879 . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧𝑦)})
151, 14wceq 1637 1 wff [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧𝑦)})
Colors of variables: wff setvar class
This definition is referenced by:  iccval  12435  elicc1  12440  iccss  12462  iccssioo  12463  iccss2  12465  iccssico  12466  iccssxr  12477  ioossicc  12480  icossicc  12482  iocssicc  12483  iccf  12494  ioounsn  12522  ioounsnOLD  12523  snunioo  12524  snunico  12525  snunioc  12526  ioodisj  12528  leordtval2  21234  iccordt  21236  lecldbas  21241  ioombl  23552  itgspliticc  23823  psercnlem2  24398  tanord1  24504  cvmliftlem10  31604  ftc1anclem7  33805  ftc1anclem8  33806  ftc1anc  33807  snunioo1  40220
  Copyright terms: Public domain W3C validator