Metamath Proof Explorer

Theorem cmetcusp1

Description: If the uniform set of a complete metric space is the uniform structure generated by its metric, then it is a complete uniform space. (Contributed by Thierry Arnoux, 15-Dec-2017)

Ref Expression
Hypotheses cmetcusp1.x ⊢X=BaseF
cmetcusp1.d ⊢D=dist⁡F↾X×X
cmetcusp1.u ⊢U=UnifSt⁡F
Assertion cmetcusp1 ⊢X≠∅∧F∈CMetSp∧U=metUnif⁡D→F∈CUnifSp

Proof

Step Hyp Ref Expression
1 cmetcusp1.x ⊢X=BaseF
2 cmetcusp1.d ⊢D=dist⁡F↾X×X
3 cmetcusp1.u ⊢U=UnifSt⁡F
4 cmsms ⊢F∈CMetSp→F∈MetSp
5 msxms ⊢F∈MetSp→F∈∞MetSp
6 4 5 syl ⊢F∈CMetSp→F∈∞MetSp
7 1 2 3 xmsusp ⊢X≠∅∧F∈∞MetSp∧U=metUnif⁡D→F∈UnifSp
8 6 7 syl3an2 ⊢X≠∅∧F∈CMetSp∧U=metUnif⁡D→F∈UnifSp
9 simpl3 ⊢X≠∅∧F∈CMetSp∧U=metUnif⁡D∧c∈Fil⁡X→U=metUnif⁡D
10 9 fveq2d ⊢X≠∅∧F∈CMetSp∧U=metUnif⁡D∧c∈Fil⁡X→CauFilU⁡U=CauFilU⁡metUnif⁡D
11 10 eleq2d ⊢X≠∅∧F∈CMetSp∧U=metUnif⁡D∧c∈Fil⁡X→c∈CauFilU⁡U↔c∈CauFilU⁡metUnif⁡D
12 simpl1 ⊢X≠∅∧F∈CMetSp∧U=metUnif⁡D∧c∈Fil⁡X→X≠∅
13 1 2 cmscmet ⊢F∈CMetSp→D∈CMet⁡X
14 cmetmet ⊢D∈CMet⁡X→D∈Met⁡X
15 metxmet ⊢D∈Met⁡X→D∈∞Met⁡X
16 13 14 15 3syl ⊢F∈CMetSp→D∈∞Met⁡X
17 16 3ad2ant2 ⊢X≠∅∧F∈CMetSp∧U=metUnif⁡D→D∈∞Met⁡X
18 17 adantr ⊢X≠∅∧F∈CMetSp∧U=metUnif⁡D∧c∈Fil⁡X→D∈∞Met⁡X
19 simpr ⊢X≠∅∧F∈CMetSp∧U=metUnif⁡D∧c∈Fil⁡X→c∈Fil⁡X
20 cfilucfil4 ⊢X≠∅∧D∈∞Met⁡X∧c∈Fil⁡X→c∈CauFilU⁡metUnif⁡D↔c∈CauFil⁡D
21 12 18 19 20 syl3anc ⊢X≠∅∧F∈CMetSp∧U=metUnif⁡D∧c∈Fil⁡X→c∈CauFilU⁡metUnif⁡D↔c∈CauFil⁡D
22 11 21 bitrd ⊢X≠∅∧F∈CMetSp∧U=metUnif⁡D∧c∈Fil⁡X→c∈CauFilU⁡U↔c∈CauFil⁡D
23 eqid ⊢MetOpen⁡D=MetOpen⁡D
24 23 iscmet ⊢D∈CMet⁡X↔D∈Met⁡X∧∀c∈CauFil⁡DMetOpen⁡DfLimc≠∅
25 24 simprbi ⊢D∈CMet⁡X→∀c∈CauFil⁡DMetOpen⁡DfLimc≠∅
26 13 25 syl ⊢F∈CMetSp→∀c∈CauFil⁡DMetOpen⁡DfLimc≠∅
27 eqid ⊢TopOpen⁡F=TopOpen⁡F
28 27 1 2 xmstopn ⊢F∈∞MetSp→TopOpen⁡F=MetOpen⁡D
29 6 28 syl ⊢F∈CMetSp→TopOpen⁡F=MetOpen⁡D
30 29 oveq1d ⊢F∈CMetSp→TopOpen⁡FfLimc=MetOpen⁡DfLimc
31 30 neeq1d ⊢F∈CMetSp→TopOpen⁡FfLimc≠∅↔MetOpen⁡DfLimc≠∅
32 31 ralbidv ⊢F∈CMetSp→∀c∈CauFil⁡DTopOpen⁡FfLimc≠∅↔∀c∈CauFil⁡DMetOpen⁡DfLimc≠∅
33 26 32 mpbird ⊢F∈CMetSp→∀c∈CauFil⁡DTopOpen⁡FfLimc≠∅
34 33 r19.21bi ⊢F∈CMetSp∧c∈CauFil⁡D→TopOpen⁡FfLimc≠∅
35 34 ex ⊢F∈CMetSp→c∈CauFil⁡D→TopOpen⁡FfLimc≠∅
36 35 3ad2ant2 ⊢X≠∅∧F∈CMetSp∧U=metUnif⁡D→c∈CauFil⁡D→TopOpen⁡FfLimc≠∅
37 36 adantr ⊢X≠∅∧F∈CMetSp∧U=metUnif⁡D∧c∈Fil⁡X→c∈CauFil⁡D→TopOpen⁡FfLimc≠∅
38 22 37 sylbid ⊢X≠∅∧F∈CMetSp∧U=metUnif⁡D∧c∈Fil⁡X→c∈CauFilU⁡U→TopOpen⁡FfLimc≠∅
39 38 ralrimiva ⊢X≠∅∧F∈CMetSp∧U=metUnif⁡D→∀c∈Fil⁡Xc∈CauFilU⁡U→TopOpen⁡FfLimc≠∅
40 1 3 27 iscusp2 ⊢F∈CUnifSp↔F∈UnifSp∧∀c∈Fil⁡Xc∈CauFilU⁡U→TopOpen⁡FfLimc≠∅
41 8 39 40 sylanbrc ⊢X≠∅∧F∈CMetSp∧U=metUnif⁡D→F∈CUnifSp