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 23292
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 23289 . 2 class CauFil
2 vd . . 3 setvar 𝑑
3 cxmt 19966 . . . . 5 class ∞Met
43crn 5264 . . . 4 class ran ∞Met
54cuni 4585 . . 3 class ran ∞Met
62cv 1633 . . . . . . . 8 class 𝑑
7 vy . . . . . . . . . 10 setvar 𝑦
87cv 1633 . . . . . . . . 9 class 𝑦
98, 8cxp 5261 . . . . . . . 8 class (𝑦 × 𝑦)
106, 9cima 5266 . . . . . . 7 class (𝑑 “ (𝑦 × 𝑦))
11 cc0 10159 . . . . . . . 8 class 0
12 vx . . . . . . . . 9 setvar 𝑥
1312cv 1633 . . . . . . . 8 class 𝑥
14 cico 12401 . . . . . . . 8 class [,)
1511, 13, 14co 6812 . . . . . . 7 class (0[,)𝑥)
1610, 15wss 3729 . . . . . 6 wff (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)
17 vf . . . . . . 7 setvar 𝑓
1817cv 1633 . . . . . 6 class 𝑓
1916, 7, 18wrex 3065 . . . . 5 wff 𝑦𝑓 (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)
20 crp 12052 . . . . 5 class +
2119, 12, 20wral 3064 . . . 4 wff 𝑥 ∈ ℝ+𝑦𝑓 (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)
226cdm 5263 . . . . . 6 class dom 𝑑
2322cdm 5263 . . . . 5 class dom dom 𝑑
24 cfil 21889 . . . . 5 class Fil
2523, 24cfv 6042 . . . 4 class (Fil‘dom dom 𝑑)
2621, 17, 25crab 3068 . . 3 class {𝑓 ∈ (Fil‘dom dom 𝑑) ∣ ∀𝑥 ∈ ℝ+𝑦𝑓 (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)}
272, 5, 26cmpt 4876 . 2 class (𝑑 ran ∞Met ↦ {𝑓 ∈ (Fil‘dom dom 𝑑) ∣ ∀𝑥 ∈ ℝ+𝑦𝑓 (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)})
281, 27wceq 1634 1 wff CauFil = (𝑑 ran ∞Met ↦ {𝑓 ∈ (Fil‘dom dom 𝑑) ∣ ∀𝑥 ∈ ℝ+𝑦𝑓 (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)})
Colors of variables: wff setvar class
This definition is referenced by:  cfilfval  23301  cfili  23305  cfilfcls  23311
  Copyright terms: Public domain W3C validator