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

Definition df-cau 22807
Description: Define a function on metric spaces whose value is the set of Cauchy sequences of the space. (Contributed by NM, 8-Sep-2006.)
Assertion
Ref Expression
df-cau Cau = (𝑑 ran ∞Met ↦ {𝑓 ∈ (dom dom 𝑑pm ℂ) ∣ ∀𝑥 ∈ ℝ+𝑗 ∈ ℤ (𝑓 ↾ (ℤ𝑗)):(ℤ𝑗)⟶((𝑓𝑗)(ball‘𝑑)𝑥)})
Distinct variable group:   𝑓,𝑑,𝑗,𝑥

Detailed syntax breakdown of Definition df-cau
StepHypRef Expression
1 cca 22804 . 2 class Cau
2 vd . . 3 setvar 𝑑
3 cxmt 19501 . . . . 5 class ∞Met
43crn 5029 . . . 4 class ran ∞Met
54cuni 4367 . . 3 class ran ∞Met
6 vj . . . . . . . . 9 setvar 𝑗
76cv 1474 . . . . . . . 8 class 𝑗
8 cuz 11522 . . . . . . . 8 class
97, 8cfv 5790 . . . . . . 7 class (ℤ𝑗)
10 vf . . . . . . . . . 10 setvar 𝑓
1110cv 1474 . . . . . . . . 9 class 𝑓
127, 11cfv 5790 . . . . . . . 8 class (𝑓𝑗)
13 vx . . . . . . . . 9 setvar 𝑥
1413cv 1474 . . . . . . . 8 class 𝑥
152cv 1474 . . . . . . . . 9 class 𝑑
16 cbl 19503 . . . . . . . . 9 class ball
1715, 16cfv 5790 . . . . . . . 8 class (ball‘𝑑)
1812, 14, 17co 6527 . . . . . . 7 class ((𝑓𝑗)(ball‘𝑑)𝑥)
1911, 9cres 5030 . . . . . . 7 class (𝑓 ↾ (ℤ𝑗))
209, 18, 19wf 5786 . . . . . 6 wff (𝑓 ↾ (ℤ𝑗)):(ℤ𝑗)⟶((𝑓𝑗)(ball‘𝑑)𝑥)
21 cz 11213 . . . . . 6 class
2220, 6, 21wrex 2897 . . . . 5 wff 𝑗 ∈ ℤ (𝑓 ↾ (ℤ𝑗)):(ℤ𝑗)⟶((𝑓𝑗)(ball‘𝑑)𝑥)
23 crp 11667 . . . . 5 class +
2422, 13, 23wral 2896 . . . 4 wff 𝑥 ∈ ℝ+𝑗 ∈ ℤ (𝑓 ↾ (ℤ𝑗)):(ℤ𝑗)⟶((𝑓𝑗)(ball‘𝑑)𝑥)
2515cdm 5028 . . . . . 6 class dom 𝑑
2625cdm 5028 . . . . 5 class dom dom 𝑑
27 cc 9791 . . . . 5 class
28 cpm 7723 . . . . 5 class pm
2926, 27, 28co 6527 . . . 4 class (dom dom 𝑑pm ℂ)
3024, 10, 29crab 2900 . . 3 class {𝑓 ∈ (dom dom 𝑑pm ℂ) ∣ ∀𝑥 ∈ ℝ+𝑗 ∈ ℤ (𝑓 ↾ (ℤ𝑗)):(ℤ𝑗)⟶((𝑓𝑗)(ball‘𝑑)𝑥)}
312, 5, 30cmpt 4638 . 2 class (𝑑 ran ∞Met ↦ {𝑓 ∈ (dom dom 𝑑pm ℂ) ∣ ∀𝑥 ∈ ℝ+𝑗 ∈ ℤ (𝑓 ↾ (ℤ𝑗)):(ℤ𝑗)⟶((𝑓𝑗)(ball‘𝑑)𝑥)})
321, 31wceq 1475 1 wff Cau = (𝑑 ran ∞Met ↦ {𝑓 ∈ (dom dom 𝑑pm ℂ) ∣ ∀𝑥 ∈ ℝ+𝑗 ∈ ℤ (𝑓 ↾ (ℤ𝑗)):(ℤ𝑗)⟶((𝑓𝑗)(ball‘𝑑)𝑥)})
Colors of variables: wff setvar class
This definition is referenced by:  caufval  22826
  Copyright terms: Public domain W3C validator