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 25171
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 25168 . 2 class Cau
2 vd . . 3 setvar 𝑑
3 cxmet 21251 . . . . 5 class ∞Met
43crn 5673 . . . 4 class ran ∞Met
54cuni 4903 . . 3 class βˆͺ ran ∞Met
6 vj . . . . . . . . 9 setvar 𝑗
76cv 1533 . . . . . . . 8 class 𝑗
8 cuz 12844 . . . . . . . 8 class β„€β‰₯
97, 8cfv 6542 . . . . . . 7 class (β„€β‰₯β€˜π‘—)
10 vf . . . . . . . . . 10 setvar 𝑓
1110cv 1533 . . . . . . . . 9 class 𝑓
127, 11cfv 6542 . . . . . . . 8 class (π‘“β€˜π‘—)
13 vx . . . . . . . . 9 setvar π‘₯
1413cv 1533 . . . . . . . 8 class π‘₯
152cv 1533 . . . . . . . . 9 class 𝑑
16 cbl 21253 . . . . . . . . 9 class ball
1715, 16cfv 6542 . . . . . . . 8 class (ballβ€˜π‘‘)
1812, 14, 17co 7414 . . . . . . 7 class ((π‘“β€˜π‘—)(ballβ€˜π‘‘)π‘₯)
1911, 9cres 5674 . . . . . . 7 class (𝑓 β†Ύ (β„€β‰₯β€˜π‘—))
209, 18, 19wf 6538 . . . . . 6 wff (𝑓 β†Ύ (β„€β‰₯β€˜π‘—)):(β„€β‰₯β€˜π‘—)⟢((π‘“β€˜π‘—)(ballβ€˜π‘‘)π‘₯)
21 cz 12580 . . . . . 6 class β„€
2220, 6, 21wrex 3065 . . . . 5 wff βˆƒπ‘— ∈ β„€ (𝑓 β†Ύ (β„€β‰₯β€˜π‘—)):(β„€β‰₯β€˜π‘—)⟢((π‘“β€˜π‘—)(ballβ€˜π‘‘)π‘₯)
23 crp 12998 . . . . 5 class ℝ+
2422, 13, 23wral 3056 . . . 4 wff βˆ€π‘₯ ∈ ℝ+ βˆƒπ‘— ∈ β„€ (𝑓 β†Ύ (β„€β‰₯β€˜π‘—)):(β„€β‰₯β€˜π‘—)⟢((π‘“β€˜π‘—)(ballβ€˜π‘‘)π‘₯)
2515cdm 5672 . . . . . 6 class dom 𝑑
2625cdm 5672 . . . . 5 class dom dom 𝑑
27 cc 11128 . . . . 5 class β„‚
28 cpm 8837 . . . . 5 class ↑pm
2926, 27, 28co 7414 . . . 4 class (dom dom 𝑑 ↑pm β„‚)
3024, 10, 29crab 3427 . . 3 class {𝑓 ∈ (dom dom 𝑑 ↑pm β„‚) ∣ βˆ€π‘₯ ∈ ℝ+ βˆƒπ‘— ∈ β„€ (𝑓 β†Ύ (β„€β‰₯β€˜π‘—)):(β„€β‰₯β€˜π‘—)⟢((π‘“β€˜π‘—)(ballβ€˜π‘‘)π‘₯)}
312, 5, 30cmpt 5225 . 2 class (𝑑 ∈ βˆͺ ran ∞Met ↦ {𝑓 ∈ (dom dom 𝑑 ↑pm β„‚) ∣ βˆ€π‘₯ ∈ ℝ+ βˆƒπ‘— ∈ β„€ (𝑓 β†Ύ (β„€β‰₯β€˜π‘—)):(β„€β‰₯β€˜π‘—)⟢((π‘“β€˜π‘—)(ballβ€˜π‘‘)π‘₯)})
321, 31wceq 1534 1 wff Cau = (𝑑 ∈ βˆͺ ran ∞Met ↦ {𝑓 ∈ (dom dom 𝑑 ↑pm β„‚) ∣ βˆ€π‘₯ ∈ ℝ+ βˆƒπ‘— ∈ β„€ (𝑓 β†Ύ (β„€β‰₯β€˜π‘—)):(β„€β‰₯β€˜π‘—)⟢((π‘“β€˜π‘—)(ballβ€˜π‘‘)π‘₯)})
Colors of variables: wff setvar class
This definition is referenced by:  caufval  25190
  Copyright terms: Public domain W3C validator