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 = Base F
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 = Base F
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 ⁡ D MetOpen ⁡ D fLim c ≠ ∅
25 24 simprbi ⊢ D ∈ CMet ⁡ X → ∀ c ∈ CauFil ⁡ D MetOpen ⁡ D fLim c ≠ ∅
26 13 25 syl ⊢ F ∈ CMetSp → ∀ c ∈ CauFil ⁡ D MetOpen ⁡ D fLim c ≠ ∅
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 ⁡ F fLim c = MetOpen ⁡ D fLim c
31 30 neeq1d ⊢ F ∈ CMetSp → TopOpen ⁡ F fLim c ≠ ∅ ↔ MetOpen ⁡ D fLim c ≠ ∅
32 31 ralbidv ⊢ F ∈ CMetSp → ∀ c ∈ CauFil ⁡ D TopOpen ⁡ F fLim c ≠ ∅ ↔ ∀ c ∈ CauFil ⁡ D MetOpen ⁡ D fLim c ≠ ∅
33 26 32 mpbird ⊢ F ∈ CMetSp → ∀ c ∈ CauFil ⁡ D TopOpen ⁡ F fLim c ≠ ∅
34 33 r19.21bi ⊢ F ∈ CMetSp ∧ c ∈ CauFil ⁡ D → TopOpen ⁡ F fLim c ≠ ∅
35 34 ex ⊢ F ∈ CMetSp → c ∈ CauFil ⁡ D → TopOpen ⁡ F fLim c ≠ ∅
36 35 3ad2ant2 ⊢ X ≠ ∅ ∧ F ∈ CMetSp ∧ U = metUnif ⁡ D → c ∈ CauFil ⁡ D → TopOpen ⁡ F fLim c ≠ ∅
37 36 adantr ⊢ X ≠ ∅ ∧ F ∈ CMetSp ∧ U = metUnif ⁡ D ∧ c ∈ Fil ⁡ X → c ∈ CauFil ⁡ D → TopOpen ⁡ F fLim c ≠ ∅
38 22 37 sylbid ⊢ X ≠ ∅ ∧ F ∈ CMetSp ∧ U = metUnif ⁡ D ∧ c ∈ Fil ⁡ X → c ∈ CauFilU ⁡ U → TopOpen ⁡ F fLim c ≠ ∅
39 38 ralrimiva ⊢ X ≠ ∅ ∧ F ∈ CMetSp ∧ U = metUnif ⁡ D → ∀ c ∈ Fil ⁡ X c ∈ CauFilU ⁡ U → TopOpen ⁡ F fLim c ≠ ∅
40 1 3 27 iscusp2 ⊢ F ∈ CUnifSp ↔ F ∈ UnifSp ∧ ∀ c ∈ Fil ⁡ X c ∈ CauFilU ⁡ U → TopOpen ⁡ F fLim c ≠ ∅
41 8 39 40 sylanbrc ⊢ X ≠ ∅ ∧ F ∈ CMetSp ∧ U = metUnif ⁡ D → F ∈ CUnifSp