Metamath Proof Explorer

Theorem iscmet

Description: The property " D is a complete metric." meaning all Cauchy filters converge to a point in the space. (Contributed by Mario Carneiro, 1-May-2014) (Revised by Mario Carneiro, 13-Oct-2015)

Ref Expression
Hypothesis iscmet.1 ⊢ J = MetOpen ⁡ D
Assertion iscmet ⊢ D ∈ CMet ⁡ X ↔ D ∈ Met ⁡ X ∧ ∀ f ∈ CauFil ⁡ D J fLim f ≠ ∅

Proof

Step Hyp Ref Expression
1 iscmet.1 ⊢ J = MetOpen ⁡ D
2 elfvex ⊢ D ∈ CMet ⁡ X → X ∈ V
3 elfvex ⊢ D ∈ Met ⁡ X → X ∈ V
4 3 adantr ⊢ D ∈ Met ⁡ X ∧ ∀ f ∈ CauFil ⁡ D J fLim f ≠ ∅ → X ∈ V
5 fveq2 ⊢ x = X → Met ⁡ x = Met ⁡ X
6 5 rabeqdv ⊢ x = X → d ∈ Met ⁡ x | ∀ f ∈ CauFil ⁡ d MetOpen ⁡ d fLim f ≠ ∅ = d ∈ Met ⁡ X | ∀ f ∈ CauFil ⁡ d MetOpen ⁡ d fLim f ≠ ∅
7 df-cmet ⊢ CMet = x ∈ V ⟼ d ∈ Met ⁡ x | ∀ f ∈ CauFil ⁡ d MetOpen ⁡ d fLim f ≠ ∅
8 fvex ⊢ Met ⁡ X ∈ V
9 8 rabex ⊢ d ∈ Met ⁡ X | ∀ f ∈ CauFil ⁡ d MetOpen ⁡ d fLim f ≠ ∅ ∈ V
10 6 7 9 fvmpt ⊢ X ∈ V → CMet ⁡ X = d ∈ Met ⁡ X | ∀ f ∈ CauFil ⁡ d MetOpen ⁡ d fLim f ≠ ∅
11 10 eleq2d ⊢ X ∈ V → D ∈ CMet ⁡ X ↔ D ∈ d ∈ Met ⁡ X | ∀ f ∈ CauFil ⁡ d MetOpen ⁡ d fLim f ≠ ∅
12 fveq2 ⊢ d = D → CauFil ⁡ d = CauFil ⁡ D
13 fveq2 ⊢ d = D → MetOpen ⁡ d = MetOpen ⁡ D
14 13 1 eqtr4di ⊢ d = D → MetOpen ⁡ d = J
15 14 oveq1d ⊢ d = D → MetOpen ⁡ d fLim f = J fLim f
16 15 neeq1d ⊢ d = D → MetOpen ⁡ d fLim f ≠ ∅ ↔ J fLim f ≠ ∅
17 12 16 raleqbidv ⊢ d = D → ∀ f ∈ CauFil ⁡ d MetOpen ⁡ d fLim f ≠ ∅ ↔ ∀ f ∈ CauFil ⁡ D J fLim f ≠ ∅
18 17 elrab ⊢ D ∈ d ∈ Met ⁡ X | ∀ f ∈ CauFil ⁡ d MetOpen ⁡ d fLim f ≠ ∅ ↔ D ∈ Met ⁡ X ∧ ∀ f ∈ CauFil ⁡ D J fLim f ≠ ∅
19 11 18 bitrdi ⊢ X ∈ V → D ∈ CMet ⁡ X ↔ D ∈ Met ⁡ X ∧ ∀ f ∈ CauFil ⁡ D J fLim f ≠ ∅
20 2 4 19 pm5.21nii ⊢ D ∈ CMet ⁡ X ↔ D ∈ Met ⁡ X ∧ ∀ f ∈ CauFil ⁡ D J fLim f ≠ ∅