Metamath Proof Explorer

Theorem cmetcusp

Description: The uniform space generated by a complete metric is a complete uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017)

Ref Expression
Assertion cmetcusp ⊢ X ≠ ∅ ∧ D ∈ CMet ⁡ X → toUnifSp ⁡ metUnif ⁡ D ∈ CUnifSp

Proof

Step Hyp Ref Expression
1 cmetmet ⊢ D ∈ CMet ⁡ X → D ∈ Met ⁡ X
2 metxmet ⊢ D ∈ Met ⁡ X → D ∈ ∞Met ⁡ X
3 xmetpsmet ⊢ D ∈ ∞Met ⁡ X → D ∈ PsMet ⁡ X
4 1 2 3 3syl ⊢ D ∈ CMet ⁡ X → D ∈ PsMet ⁡ X
5 4 anim2i ⊢ X ≠ ∅ ∧ D ∈ CMet ⁡ X → X ≠ ∅ ∧ D ∈ PsMet ⁡ X
6 metuust ⊢ X ≠ ∅ ∧ D ∈ PsMet ⁡ X → metUnif ⁡ D ∈ UnifOn ⁡ X
7 eqid ⊢ toUnifSp ⁡ metUnif ⁡ D = toUnifSp ⁡ metUnif ⁡ D
8 7 tususp ⊢ metUnif ⁡ D ∈ UnifOn ⁡ X → toUnifSp ⁡ metUnif ⁡ D ∈ UnifSp
9 5 6 8 3syl ⊢ X ≠ ∅ ∧ D ∈ CMet ⁡ X → toUnifSp ⁡ metUnif ⁡ D ∈ UnifSp
10 simpll ⊢ X ≠ ∅ ∧ D ∈ CMet ⁡ X ∧ c ∈ Fil ⁡ Base toUnifSp ⁡ metUnif ⁡ D ∧ c ∈ CauFilU ⁡ UnifSt ⁡ toUnifSp ⁡ metUnif ⁡ D → X ≠ ∅ ∧ D ∈ CMet ⁡ X
11 10 simprd ⊢ X ≠ ∅ ∧ D ∈ CMet ⁡ X ∧ c ∈ Fil ⁡ Base toUnifSp ⁡ metUnif ⁡ D ∧ c ∈ CauFilU ⁡ UnifSt ⁡ toUnifSp ⁡ metUnif ⁡ D → D ∈ CMet ⁡ X
12 1 2 syl ⊢ D ∈ CMet ⁡ X → D ∈ ∞Met ⁡ X
13 12 ad3antlr ⊢ X ≠ ∅ ∧ D ∈ CMet ⁡ X ∧ c ∈ Fil ⁡ Base toUnifSp ⁡ metUnif ⁡ D ∧ c ∈ CauFilU ⁡ UnifSt ⁡ toUnifSp ⁡ metUnif ⁡ D → D ∈ ∞Met ⁡ X
14 7 tusbas ⊢ metUnif ⁡ D ∈ UnifOn ⁡ X → X = Base toUnifSp ⁡ metUnif ⁡ D
15 14 fveq2d ⊢ metUnif ⁡ D ∈ UnifOn ⁡ X → Fil ⁡ X = Fil ⁡ Base toUnifSp ⁡ metUnif ⁡ D
16 15 eleq2d ⊢ metUnif ⁡ D ∈ UnifOn ⁡ X → c ∈ Fil ⁡ X ↔ c ∈ Fil ⁡ Base toUnifSp ⁡ metUnif ⁡ D
17 5 6 16 3syl ⊢ X ≠ ∅ ∧ D ∈ CMet ⁡ X → c ∈ Fil ⁡ X ↔ c ∈ Fil ⁡ Base toUnifSp ⁡ metUnif ⁡ D
18 17 biimpar ⊢ X ≠ ∅ ∧ D ∈ CMet ⁡ X ∧ c ∈ Fil ⁡ Base toUnifSp ⁡ metUnif ⁡ D → c ∈ Fil ⁡ X
19 18 adantr ⊢ X ≠ ∅ ∧ D ∈ CMet ⁡ X ∧ c ∈ Fil ⁡ Base toUnifSp ⁡ metUnif ⁡ D ∧ c ∈ CauFilU ⁡ UnifSt ⁡ toUnifSp ⁡ metUnif ⁡ D → c ∈ Fil ⁡ X
20 7 tususs ⊢ metUnif ⁡ D ∈ UnifOn ⁡ X → metUnif ⁡ D = UnifSt ⁡ toUnifSp ⁡ metUnif ⁡ D
21 20 fveq2d ⊢ metUnif ⁡ D ∈ UnifOn ⁡ X → CauFilU ⁡ metUnif ⁡ D = CauFilU ⁡ UnifSt ⁡ toUnifSp ⁡ metUnif ⁡ D
22 5 6 21 3syl ⊢ X ≠ ∅ ∧ D ∈ CMet ⁡ X → CauFilU ⁡ metUnif ⁡ D = CauFilU ⁡ UnifSt ⁡ toUnifSp ⁡ metUnif ⁡ D
23 22 eleq2d ⊢ X ≠ ∅ ∧ D ∈ CMet ⁡ X → c ∈ CauFilU ⁡ metUnif ⁡ D ↔ c ∈ CauFilU ⁡ UnifSt ⁡ toUnifSp ⁡ metUnif ⁡ D
24 23 biimpar ⊢ X ≠ ∅ ∧ D ∈ CMet ⁡ X ∧ c ∈ CauFilU ⁡ UnifSt ⁡ toUnifSp ⁡ metUnif ⁡ D → c ∈ CauFilU ⁡ metUnif ⁡ D
25 24 adantlr ⊢ X ≠ ∅ ∧ D ∈ CMet ⁡ X ∧ c ∈ Fil ⁡ Base toUnifSp ⁡ metUnif ⁡ D ∧ c ∈ CauFilU ⁡ UnifSt ⁡ toUnifSp ⁡ metUnif ⁡ D → c ∈ CauFilU ⁡ metUnif ⁡ D
26 cfilucfil2 ⊢ X ≠ ∅ ∧ D ∈ PsMet ⁡ X → c ∈ CauFilU ⁡ metUnif ⁡ D ↔ c ∈ fBas ⁡ X ∧ ∀ x ∈ ℝ + ∃ y ∈ c D y × y ⊆ 0 x
27 5 26 syl ⊢ X ≠ ∅ ∧ D ∈ CMet ⁡ X → c ∈ CauFilU ⁡ metUnif ⁡ D ↔ c ∈ fBas ⁡ X ∧ ∀ x ∈ ℝ + ∃ y ∈ c D y × y ⊆ 0 x
28 27 simplbda ⊢ X ≠ ∅ ∧ D ∈ CMet ⁡ X ∧ c ∈ CauFilU ⁡ metUnif ⁡ D → ∀ x ∈ ℝ + ∃ y ∈ c D y × y ⊆ 0 x
29 10 25 28 syl2anc ⊢ X ≠ ∅ ∧ D ∈ CMet ⁡ X ∧ c ∈ Fil ⁡ Base toUnifSp ⁡ metUnif ⁡ D ∧ c ∈ CauFilU ⁡ UnifSt ⁡ toUnifSp ⁡ metUnif ⁡ D → ∀ x ∈ ℝ + ∃ y ∈ c D y × y ⊆ 0 x
30 iscfil ⊢ D ∈ ∞Met ⁡ X → c ∈ CauFil ⁡ D ↔ c ∈ Fil ⁡ X ∧ ∀ x ∈ ℝ + ∃ y ∈ c D y × y ⊆ 0 x
31 30 biimpar ⊢ D ∈ ∞Met ⁡ X ∧ c ∈ Fil ⁡ X ∧ ∀ x ∈ ℝ + ∃ y ∈ c D y × y ⊆ 0 x → c ∈ CauFil ⁡ D
32 13 19 29 31 syl12anc ⊢ X ≠ ∅ ∧ D ∈ CMet ⁡ X ∧ c ∈ Fil ⁡ Base toUnifSp ⁡ metUnif ⁡ D ∧ c ∈ CauFilU ⁡ UnifSt ⁡ toUnifSp ⁡ metUnif ⁡ D → c ∈ CauFil ⁡ D
33 eqid ⊢ MetOpen ⁡ D = MetOpen ⁡ D
34 33 cmetcvg ⊢ D ∈ CMet ⁡ X ∧ c ∈ CauFil ⁡ D → MetOpen ⁡ D fLim c ≠ ∅
35 11 32 34 syl2anc ⊢ X ≠ ∅ ∧ D ∈ CMet ⁡ X ∧ c ∈ Fil ⁡ Base toUnifSp ⁡ metUnif ⁡ D ∧ c ∈ CauFilU ⁡ UnifSt ⁡ toUnifSp ⁡ metUnif ⁡ D → MetOpen ⁡ D fLim c ≠ ∅
36 eqid ⊢ unifTop ⁡ metUnif ⁡ D = unifTop ⁡ metUnif ⁡ D
37 7 36 tustopn ⊢ metUnif ⁡ D ∈ UnifOn ⁡ X → unifTop ⁡ metUnif ⁡ D = TopOpen ⁡ toUnifSp ⁡ metUnif ⁡ D
38 5 6 37 3syl ⊢ X ≠ ∅ ∧ D ∈ CMet ⁡ X → unifTop ⁡ metUnif ⁡ D = TopOpen ⁡ toUnifSp ⁡ metUnif ⁡ D
39 12 anim2i ⊢ X ≠ ∅ ∧ D ∈ CMet ⁡ X → X ≠ ∅ ∧ D ∈ ∞Met ⁡ X
40 xmetutop ⊢ X ≠ ∅ ∧ D ∈ ∞Met ⁡ X → unifTop ⁡ metUnif ⁡ D = MetOpen ⁡ D
41 39 40 syl ⊢ X ≠ ∅ ∧ D ∈ CMet ⁡ X → unifTop ⁡ metUnif ⁡ D = MetOpen ⁡ D
42 38 41 eqtr3d ⊢ X ≠ ∅ ∧ D ∈ CMet ⁡ X → TopOpen ⁡ toUnifSp ⁡ metUnif ⁡ D = MetOpen ⁡ D
43 42 oveq1d ⊢ X ≠ ∅ ∧ D ∈ CMet ⁡ X → TopOpen ⁡ toUnifSp ⁡ metUnif ⁡ D fLim c = MetOpen ⁡ D fLim c
44 43 neeq1d ⊢ X ≠ ∅ ∧ D ∈ CMet ⁡ X → TopOpen ⁡ toUnifSp ⁡ metUnif ⁡ D fLim c ≠ ∅ ↔ MetOpen ⁡ D fLim c ≠ ∅
45 44 biimpar ⊢ X ≠ ∅ ∧ D ∈ CMet ⁡ X ∧ MetOpen ⁡ D fLim c ≠ ∅ → TopOpen ⁡ toUnifSp ⁡ metUnif ⁡ D fLim c ≠ ∅
46 10 35 45 syl2anc ⊢ X ≠ ∅ ∧ D ∈ CMet ⁡ X ∧ c ∈ Fil ⁡ Base toUnifSp ⁡ metUnif ⁡ D ∧ c ∈ CauFilU ⁡ UnifSt ⁡ toUnifSp ⁡ metUnif ⁡ D → TopOpen ⁡ toUnifSp ⁡ metUnif ⁡ D fLim c ≠ ∅
47 46 ex ⊢ X ≠ ∅ ∧ D ∈ CMet ⁡ X ∧ c ∈ Fil ⁡ Base toUnifSp ⁡ metUnif ⁡ D → c ∈ CauFilU ⁡ UnifSt ⁡ toUnifSp ⁡ metUnif ⁡ D → TopOpen ⁡ toUnifSp ⁡ metUnif ⁡ D fLim c ≠ ∅
48 47 ralrimiva ⊢ X ≠ ∅ ∧ D ∈ CMet ⁡ X → ∀ c ∈ Fil ⁡ Base toUnifSp ⁡ metUnif ⁡ D c ∈ CauFilU ⁡ UnifSt ⁡ toUnifSp ⁡ metUnif ⁡ D → TopOpen ⁡ toUnifSp ⁡ metUnif ⁡ D fLim c ≠ ∅
49 iscusp ⊢ toUnifSp ⁡ metUnif ⁡ D ∈ CUnifSp ↔ toUnifSp ⁡ metUnif ⁡ D ∈ UnifSp ∧ ∀ c ∈ Fil ⁡ Base toUnifSp ⁡ metUnif ⁡ D c ∈ CauFilU ⁡ UnifSt ⁡ toUnifSp ⁡ metUnif ⁡ D → TopOpen ⁡ toUnifSp ⁡ metUnif ⁡ D fLim c ≠ ∅
50 9 48 49 sylanbrc ⊢ X ≠ ∅ ∧ D ∈ CMet ⁡ X → toUnifSp ⁡ metUnif ⁡ D ∈ CUnifSp