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 22775
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 22772 . 2 class CauFil
2 vd . . 3 setvar 𝑑
3 cxmt 19494 . . . . 5 class ∞Met
43crn 5025 . . . 4 class ran ∞Met
54cuni 4362 . . 3 class ran ∞Met
62cv 1473 . . . . . . . 8 class 𝑑
7 vy . . . . . . . . . 10 setvar 𝑦
87cv 1473 . . . . . . . . 9 class 𝑦
98, 8cxp 5022 . . . . . . . 8 class (𝑦 × 𝑦)
106, 9cima 5027 . . . . . . 7 class (𝑑 “ (𝑦 × 𝑦))
11 cc0 9788 . . . . . . . 8 class 0
12 vx . . . . . . . . 9 setvar 𝑥
1312cv 1473 . . . . . . . 8 class 𝑥
14 cico 12000 . . . . . . . 8 class [,)
1511, 13, 14co 6523 . . . . . . 7 class (0[,)𝑥)
1610, 15wss 3535 . . . . . 6 wff (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)
17 vf . . . . . . 7 setvar 𝑓
1817cv 1473 . . . . . 6 class 𝑓
1916, 7, 18wrex 2892 . . . . 5 wff 𝑦𝑓 (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)
20 crp 11660 . . . . 5 class +
2119, 12, 20wral 2891 . . . 4 wff 𝑥 ∈ ℝ+𝑦𝑓 (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)
226cdm 5024 . . . . . 6 class dom 𝑑
2322cdm 5024 . . . . 5 class dom dom 𝑑
24 cfil 21397 . . . . 5 class Fil
2523, 24cfv 5786 . . . 4 class (Fil‘dom dom 𝑑)
2621, 17, 25crab 2895 . . 3 class {𝑓 ∈ (Fil‘dom dom 𝑑) ∣ ∀𝑥 ∈ ℝ+𝑦𝑓 (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)}
272, 5, 26cmpt 4633 . 2 class (𝑑 ran ∞Met ↦ {𝑓 ∈ (Fil‘dom dom 𝑑) ∣ ∀𝑥 ∈ ℝ+𝑦𝑓 (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)})
281, 27wceq 1474 1 wff CauFil = (𝑑 ran ∞Met ↦ {𝑓 ∈ (Fil‘dom dom 𝑑) ∣ ∀𝑥 ∈ ℝ+𝑦𝑓 (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)})
Colors of variables: wff setvar class
This definition is referenced by:  cfilfval  22784  cfili  22788  cfilfcls  22794
  Copyright terms: Public domain W3C validator