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

Definition df-cfil 22861
Description: Define the set of Cauchy filters on a metric space. A Cauchy filter is a filter on the set such that for every 0 < 𝑥 there is an element of the filter whose metric diameter is less than 𝑥. (Contributed by Mario Carneiro, 13-Oct-2015.)
Assertion
Ref Expression
df-cfil CauFil = (𝑑 ran ∞Met ↦ {𝑓 ∈ (Fil‘dom dom 𝑑) ∣ ∀𝑥 ∈ ℝ+𝑦𝑓 (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)})
Distinct variable group:   𝑓,𝑑,𝑥,𝑦

Detailed syntax breakdown of Definition df-cfil
StepHypRef Expression
1 ccfil 22858 . 2 class CauFil
2 vd . . 3 setvar 𝑑
3 cxmt 19552 . . . . 5 class ∞Met
43crn 5039 . . . 4 class ran ∞Met
54cuni 4372 . . 3 class ran ∞Met
62cv 1474 . . . . . . . 8 class 𝑑
7 vy . . . . . . . . . 10 setvar 𝑦
87cv 1474 . . . . . . . . 9 class 𝑦
98, 8cxp 5036 . . . . . . . 8 class (𝑦 × 𝑦)
106, 9cima 5041 . . . . . . 7 class (𝑑 “ (𝑦 × 𝑦))
11 cc0 9815 . . . . . . . 8 class 0
12 vx . . . . . . . . 9 setvar 𝑥
1312cv 1474 . . . . . . . 8 class 𝑥
14 cico 12048 . . . . . . . 8 class [,)
1511, 13, 14co 6549 . . . . . . 7 class (0[,)𝑥)
1610, 15wss 3540 . . . . . 6 wff (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)
17 vf . . . . . . 7 setvar 𝑓
1817cv 1474 . . . . . 6 class 𝑓
1916, 7, 18wrex 2897 . . . . 5 wff 𝑦𝑓 (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)
20 crp 11708 . . . . 5 class +
2119, 12, 20wral 2896 . . . 4 wff 𝑥 ∈ ℝ+𝑦𝑓 (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)
226cdm 5038 . . . . . 6 class dom 𝑑
2322cdm 5038 . . . . 5 class dom dom 𝑑
24 cfil 21459 . . . . 5 class Fil
2523, 24cfv 5804 . . . 4 class (Fil‘dom dom 𝑑)
2621, 17, 25crab 2900 . . 3 class {𝑓 ∈ (Fil‘dom dom 𝑑) ∣ ∀𝑥 ∈ ℝ+𝑦𝑓 (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)}
272, 5, 26cmpt 4643 . 2 class (𝑑 ran ∞Met ↦ {𝑓 ∈ (Fil‘dom dom 𝑑) ∣ ∀𝑥 ∈ ℝ+𝑦𝑓 (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)})
281, 27wceq 1475 1 wff CauFil = (𝑑 ran ∞Met ↦ {𝑓 ∈ (Fil‘dom dom 𝑑) ∣ ∀𝑥 ∈ ℝ+𝑦𝑓 (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)})
Colors of variables: wff setvar class
This definition is referenced by:  cfilfval  22870  cfili  22874  cfilfcls  22880
  Copyright terms: Public domain W3C validator