Metamath Proof Explorer

Theorem cfilfval

Description: The set of Cauchy filters on a metric space. (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Assertion cfilfval ⊢ D ∈ ∞Met ⁡ X → CauFil ⁡ D = f ∈ Fil ⁡ X | ∀ x ∈ ℝ + ∃ y ∈ f D y × y ⊆ 0 x

Proof

Step Hyp Ref Expression
1 fvssunirn ⊢ ∞Met ⁡ X ⊆ ⋃ ran ⁡ ∞Met
2 1 sseli ⊢ D ∈ ∞Met ⁡ X → D ∈ ⋃ ran ⁡ ∞Met
3 dmeq ⊢ d = D → dom ⁡ d = dom ⁡ D
4 3 dmeqd ⊢ d = D → dom ⁡ dom ⁡ d = dom ⁡ dom ⁡ D
5 4 fveq2d ⊢ d = D → Fil ⁡ dom ⁡ dom ⁡ d = Fil ⁡ dom ⁡ dom ⁡ D
6 imaeq1 ⊢ d = D → d y × y = D y × y
7 6 sseq1d ⊢ d = D → d y × y ⊆ 0 x ↔ D y × y ⊆ 0 x
8 7 rexbidv ⊢ d = D → ∃ y ∈ f d y × y ⊆ 0 x ↔ ∃ y ∈ f D y × y ⊆ 0 x
9 8 ralbidv ⊢ d = D → ∀ x ∈ ℝ + ∃ y ∈ f d y × y ⊆ 0 x ↔ ∀ x ∈ ℝ + ∃ y ∈ f D y × y ⊆ 0 x
10 5 9 rabeqbidv ⊢ d = D → f ∈ Fil ⁡ dom ⁡ dom ⁡ d | ∀ x ∈ ℝ + ∃ y ∈ f d y × y ⊆ 0 x = f ∈ Fil ⁡ dom ⁡ dom ⁡ D | ∀ x ∈ ℝ + ∃ y ∈ f D y × y ⊆ 0 x
11 df-cfil ⊢ CauFil = d ∈ ⋃ ran ⁡ ∞Met ⟼ f ∈ Fil ⁡ dom ⁡ dom ⁡ d | ∀ x ∈ ℝ + ∃ y ∈ f d y × y ⊆ 0 x
12 fvex ⊢ Fil ⁡ dom ⁡ dom ⁡ D ∈ V
13 12 rabex ⊢ f ∈ Fil ⁡ dom ⁡ dom ⁡ D | ∀ x ∈ ℝ + ∃ y ∈ f D y × y ⊆ 0 x ∈ V
14 10 11 13 fvmpt ⊢ D ∈ ⋃ ran ⁡ ∞Met → CauFil ⁡ D = f ∈ Fil ⁡ dom ⁡ dom ⁡ D | ∀ x ∈ ℝ + ∃ y ∈ f D y × y ⊆ 0 x
15 2 14 syl ⊢ D ∈ ∞Met ⁡ X → CauFil ⁡ D = f ∈ Fil ⁡ dom ⁡ dom ⁡ D | ∀ x ∈ ℝ + ∃ y ∈ f D y × y ⊆ 0 x
16 xmetdmdm ⊢ D ∈ ∞Met ⁡ X → X = dom ⁡ dom ⁡ D
17 16 fveq2d ⊢ D ∈ ∞Met ⁡ X → Fil ⁡ X = Fil ⁡ dom ⁡ dom ⁡ D
18 17 rabeqdv ⊢ D ∈ ∞Met ⁡ X → f ∈ Fil ⁡ X | ∀ x ∈ ℝ + ∃ y ∈ f D y × y ⊆ 0 x = f ∈ Fil ⁡ dom ⁡ dom ⁡ D | ∀ x ∈ ℝ + ∃ y ∈ f D y × y ⊆ 0 x
19 15 18 eqtr4d ⊢ D ∈ ∞Met ⁡ X → CauFil ⁡ D = f ∈ Fil ⁡ X | ∀ x ∈ ℝ + ∃ y ∈ f D y × y ⊆ 0 x