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 23264
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 23261 . 2 class Cau
2 vd . . 3 setvar 𝑑
3 cxmt 19937 . . . . 5 class ∞Met
43crn 5310 . . . 4 class ran ∞Met
54cuni 4628 . . 3 class ran ∞Met
6 vj . . . . . . . . 9 setvar 𝑗
76cv 1636 . . . . . . . 8 class 𝑗
8 cuz 11902 . . . . . . . 8 class
97, 8cfv 6099 . . . . . . 7 class (ℤ𝑗)
10 vf . . . . . . . . . 10 setvar 𝑓
1110cv 1636 . . . . . . . . 9 class 𝑓
127, 11cfv 6099 . . . . . . . 8 class (𝑓𝑗)
13 vx . . . . . . . . 9 setvar 𝑥
1413cv 1636 . . . . . . . 8 class 𝑥
152cv 1636 . . . . . . . . 9 class 𝑑
16 cbl 19939 . . . . . . . . 9 class ball
1715, 16cfv 6099 . . . . . . . 8 class (ball‘𝑑)
1812, 14, 17co 6872 . . . . . . 7 class ((𝑓𝑗)(ball‘𝑑)𝑥)
1911, 9cres 5311 . . . . . . 7 class (𝑓 ↾ (ℤ𝑗))
209, 18, 19wf 6095 . . . . . 6 wff (𝑓 ↾ (ℤ𝑗)):(ℤ𝑗)⟶((𝑓𝑗)(ball‘𝑑)𝑥)
21 cz 11641 . . . . . 6 class
2220, 6, 21wrex 3095 . . . . 5 wff 𝑗 ∈ ℤ (𝑓 ↾ (ℤ𝑗)):(ℤ𝑗)⟶((𝑓𝑗)(ball‘𝑑)𝑥)
23 crp 12044 . . . . 5 class +
2422, 13, 23wral 3094 . . . 4 wff 𝑥 ∈ ℝ+𝑗 ∈ ℤ (𝑓 ↾ (ℤ𝑗)):(ℤ𝑗)⟶((𝑓𝑗)(ball‘𝑑)𝑥)
2515cdm 5309 . . . . . 6 class dom 𝑑
2625cdm 5309 . . . . 5 class dom dom 𝑑
27 cc 10217 . . . . 5 class
28 cpm 8091 . . . . 5 class pm
2926, 27, 28co 6872 . . . 4 class (dom dom 𝑑pm ℂ)
3024, 10, 29crab 3098 . . 3 class {𝑓 ∈ (dom dom 𝑑pm ℂ) ∣ ∀𝑥 ∈ ℝ+𝑗 ∈ ℤ (𝑓 ↾ (ℤ𝑗)):(ℤ𝑗)⟶((𝑓𝑗)(ball‘𝑑)𝑥)}
312, 5, 30cmpt 4921 . 2 class (𝑑 ran ∞Met ↦ {𝑓 ∈ (dom dom 𝑑pm ℂ) ∣ ∀𝑥 ∈ ℝ+𝑗 ∈ ℤ (𝑓 ↾ (ℤ𝑗)):(ℤ𝑗)⟶((𝑓𝑗)(ball‘𝑑)𝑥)})
321, 31wceq 1637 1 wff Cau = (𝑑 ran ∞Met ↦ {𝑓 ∈ (dom dom 𝑑pm ℂ) ∣ ∀𝑥 ∈ ℝ+𝑗 ∈ ℤ (𝑓 ↾ (ℤ𝑗)):(ℤ𝑗)⟶((𝑓𝑗)(ball‘𝑑)𝑥)})
Colors of variables: wff setvar class
This definition is referenced by:  caufval  23283
  Copyright terms: Public domain W3C validator