Metamath Proof Explorer

Theorem equivcmet

Description: If two metrics are strongly equivalent, one is complete iff the other is. Unlike equivcau , metss2 , this theorem does not have a one-directional form - it is possible for a metric C that is strongly finer than the complete metric D to be incomplete and vice versa. Consider D = the metric on RR induced by the usual homeomorphism from ( 0 , 1 ) against the usual metric C on RR and against the discrete metric E on RR . Then both C and E are complete but D is not, and C is strongly finer than D , which is strongly finer than E . (Contributed by Mario Carneiro, 15-Sep-2015)

Ref Expression
Hypotheses equivcmet.1 ⊢φ→C∈Met⁡X
equivcmet.2 ⊢φ→D∈Met⁡X
equivcmet.3 ⊢φ→R∈ℝ+
equivcmet.4 ⊢φ→S∈ℝ+
equivcmet.5 ⊢φ∧x∈X∧y∈X→xCy≤R⁢xDy
equivcmet.6 ⊢φ∧x∈X∧y∈X→xDy≤S⁢xCy
Assertion equivcmet ⊢φ→C∈CMet⁡X↔D∈CMet⁡X

Proof

Step Hyp Ref Expression
1 equivcmet.1 ⊢φ→C∈Met⁡X
2 equivcmet.2 ⊢φ→D∈Met⁡X
3 equivcmet.3 ⊢φ→R∈ℝ+
4 equivcmet.4 ⊢φ→S∈ℝ+
5 equivcmet.5 ⊢φ∧x∈X∧y∈X→xCy≤R⁢xDy
6 equivcmet.6 ⊢φ∧x∈X∧y∈X→xDy≤S⁢xCy
7 1 2 2thd ⊢φ→C∈Met⁡X↔D∈Met⁡X
8 2 1 4 6 equivcfil ⊢φ→CauFil⁡C⊆CauFil⁡D
9 1 2 3 5 equivcfil ⊢φ→CauFil⁡D⊆CauFil⁡C
10 8 9 eqssd ⊢φ→CauFil⁡C=CauFil⁡D
11 eqid ⊢MetOpen⁡C=MetOpen⁡C
12 eqid ⊢MetOpen⁡D=MetOpen⁡D
13 11 12 1 2 3 5 metss2 ⊢φ→MetOpen⁡C⊆MetOpen⁡D
14 12 11 2 1 4 6 metss2 ⊢φ→MetOpen⁡D⊆MetOpen⁡C
15 13 14 eqssd ⊢φ→MetOpen⁡C=MetOpen⁡D
16 15 oveq1d ⊢φ→MetOpen⁡CfLimf=MetOpen⁡DfLimf
17 16 neeq1d ⊢φ→MetOpen⁡CfLimf≠∅↔MetOpen⁡DfLimf≠∅
18 10 17 raleqbidv ⊢φ→∀f∈CauFil⁡CMetOpen⁡CfLimf≠∅↔∀f∈CauFil⁡DMetOpen⁡DfLimf≠∅
19 7 18 anbi12d ⊢φ→C∈Met⁡X∧∀f∈CauFil⁡CMetOpen⁡CfLimf≠∅↔D∈Met⁡X∧∀f∈CauFil⁡DMetOpen⁡DfLimf≠∅
20 11 iscmet ⊢C∈CMet⁡X↔C∈Met⁡X∧∀f∈CauFil⁡CMetOpen⁡CfLimf≠∅
21 12 iscmet ⊢D∈CMet⁡X↔D∈Met⁡X∧∀f∈CauFil⁡DMetOpen⁡DfLimf≠∅
22 19 20 21 3bitr4g ⊢φ→C∈CMet⁡X↔D∈CMet⁡X