This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-cfil

Description: Define the set of Cauchy filters on a given extended metric space. A Cauchy filter is a filter on the set such that for every 0 < x there is an element of the filter whose metric diameter is less than x . (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Assertion df-cfil ⊢ CauFil = d ∈ ⋃ ran ⁡ ∞Met ⟼ f ∈ Fil ⁡ dom ⁡ dom ⁡ d | ∀ x ∈ ℝ + ∃ y ∈ f d y × y ⊆ 0 x

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccfil class CauFil
1 vd setvar d
2 cxmet class ∞Met
3 2 crn class ran ⁡ ∞Met
4 3 cuni class ⋃ ran ⁡ ∞Met
5 vf setvar f
6 cfil class Fil
7 1 cv setvar d
8 7 cdm class dom ⁡ d
9 8 cdm class dom ⁡ dom ⁡ d
10 9 6 cfv class Fil ⁡ dom ⁡ dom ⁡ d
11 vx setvar x
12 crp class ℝ +
13 vy setvar y
14 5 cv setvar f
15 13 cv setvar y
16 15 15 cxp class y × y
17 7 16 cima class d y × y
18 cc0 class 0
19 cico class .
20 11 cv setvar x
21 18 20 19 co class 0 x
22 17 21 wss wff d y × y ⊆ 0 x
23 22 13 14 wrex wff ∃ y ∈ f d y × y ⊆ 0 x
24 23 11 12 wral wff ∀ x ∈ ℝ + ∃ y ∈ f d y × y ⊆ 0 x
25 24 5 10 crab class f ∈ Fil ⁡ dom ⁡ dom ⁡ d | ∀ x ∈ ℝ + ∃ y ∈ f d y × y ⊆ 0 x
26 1 4 25 cmpt class d ∈ ⋃ ran ⁡ ∞Met ⟼ f ∈ Fil ⁡ dom ⁡ dom ⁡ d | ∀ x ∈ ℝ + ∃ y ∈ f d y × y ⊆ 0 x
27 0 26 wceq wff CauFil = d ∈ ⋃ ran ⁡ ∞Met ⟼ f ∈ Fil ⁡ dom ⁡ dom ⁡ d | ∀ x ∈ ℝ + ∃ y ∈ f d y × y ⊆ 0 x