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