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

Definition df-cau 23867
 Description: Define the set of Cauchy sequences on a given extended metric 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 ccau 23864 . 2 class Cau
2 vd . . 3 setvar 𝑑
3 cxmet 20079 . . . . 5 class ∞Met
43crn 5520 . . . 4 class ran ∞Met
54cuni 4800 . . 3 class ran ∞Met
6 vj . . . . . . . . 9 setvar 𝑗
76cv 1537 . . . . . . . 8 class 𝑗
8 cuz 12233 . . . . . . . 8 class
97, 8cfv 6324 . . . . . . 7 class (ℤ𝑗)
10 vf . . . . . . . . . 10 setvar 𝑓
1110cv 1537 . . . . . . . . 9 class 𝑓
127, 11cfv 6324 . . . . . . . 8 class (𝑓𝑗)
13 vx . . . . . . . . 9 setvar 𝑥
1413cv 1537 . . . . . . . 8 class 𝑥
152cv 1537 . . . . . . . . 9 class 𝑑
16 cbl 20081 . . . . . . . . 9 class ball
1715, 16cfv 6324 . . . . . . . 8 class (ball‘𝑑)
1812, 14, 17co 7135 . . . . . . 7 class ((𝑓𝑗)(ball‘𝑑)𝑥)
1911, 9cres 5521 . . . . . . 7 class (𝑓 ↾ (ℤ𝑗))
209, 18, 19wf 6320 . . . . . 6 wff (𝑓 ↾ (ℤ𝑗)):(ℤ𝑗)⟶((𝑓𝑗)(ball‘𝑑)𝑥)
21 cz 11971 . . . . . 6 class
2220, 6, 21wrex 3107 . . . . 5 wff 𝑗 ∈ ℤ (𝑓 ↾ (ℤ𝑗)):(ℤ𝑗)⟶((𝑓𝑗)(ball‘𝑑)𝑥)
23 crp 12379 . . . . 5 class +
2422, 13, 23wral 3106 . . . 4 wff 𝑥 ∈ ℝ+𝑗 ∈ ℤ (𝑓 ↾ (ℤ𝑗)):(ℤ𝑗)⟶((𝑓𝑗)(ball‘𝑑)𝑥)
2515cdm 5519 . . . . . 6 class dom 𝑑
2625cdm 5519 . . . . 5 class dom dom 𝑑
27 cc 10526 . . . . 5 class
28 cpm 8392 . . . . 5 class pm
2926, 27, 28co 7135 . . . 4 class (dom dom 𝑑pm ℂ)
3024, 10, 29crab 3110 . . 3 class {𝑓 ∈ (dom dom 𝑑pm ℂ) ∣ ∀𝑥 ∈ ℝ+𝑗 ∈ ℤ (𝑓 ↾ (ℤ𝑗)):(ℤ𝑗)⟶((𝑓𝑗)(ball‘𝑑)𝑥)}
312, 5, 30cmpt 5110 . 2 class (𝑑 ran ∞Met ↦ {𝑓 ∈ (dom dom 𝑑pm ℂ) ∣ ∀𝑥 ∈ ℝ+𝑗 ∈ ℤ (𝑓 ↾ (ℤ𝑗)):(ℤ𝑗)⟶((𝑓𝑗)(ball‘𝑑)𝑥)})
321, 31wceq 1538 1 wff Cau = (𝑑 ran ∞Met ↦ {𝑓 ∈ (dom dom 𝑑pm ℂ) ∣ ∀𝑥 ∈ ℝ+𝑗 ∈ ℤ (𝑓 ↾ (ℤ𝑗)):(ℤ𝑗)⟶((𝑓𝑗)(ball‘𝑑)𝑥)})
 Colors of variables: wff setvar class This definition is referenced by:  caufval  23886
 Copyright terms: Public domain W3C validator