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