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⁡DJfLimf≠∅

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⁡DJfLimf≠∅→X∈V
5 fveq2 ⊢x=X→Met⁡x=Met⁡X
6 5 rabeqdv ⊢x=X→d∈Met⁡x|∀f∈CauFil⁡dMetOpen⁡dfLimf≠∅=d∈Met⁡X|∀f∈CauFil⁡dMetOpen⁡dfLimf≠∅
7 df-cmet ⊢CMet=x∈V⟼d∈Met⁡x|∀f∈CauFil⁡dMetOpen⁡dfLimf≠∅
8 fvex ⊢Met⁡X∈V
9 8 rabex ⊢d∈Met⁡X|∀f∈CauFil⁡dMetOpen⁡dfLimf≠∅∈V
10 6 7 9 fvmpt ⊢X∈V→CMet⁡X=d∈Met⁡X|∀f∈CauFil⁡dMetOpen⁡dfLimf≠∅
11 10 eleq2d ⊢X∈V→D∈CMet⁡X↔D∈d∈Met⁡X|∀f∈CauFil⁡dMetOpen⁡dfLimf≠∅
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⁡dfLimf=JfLimf
16 15 neeq1d ⊢d=D→MetOpen⁡dfLimf≠∅↔JfLimf≠∅
17 12 16 raleqbidv ⊢d=D→∀f∈CauFil⁡dMetOpen⁡dfLimf≠∅↔∀f∈CauFil⁡DJfLimf≠∅
18 17 elrab ⊢D∈d∈Met⁡X|∀f∈CauFil⁡dMetOpen⁡dfLimf≠∅↔D∈Met⁡X∧∀f∈CauFil⁡DJfLimf≠∅
19 11 18 bitrdi ⊢X∈V→D∈CMet⁡X↔D∈Met⁡X∧∀f∈CauFil⁡DJfLimf≠∅
20 2 4 19 pm5.21nii ⊢D∈CMet⁡X↔D∈Met⁡X∧∀f∈CauFil⁡DJfLimf≠∅