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. X ) )
cmetcusp1.u 
|- U = ( UnifSt ` F )
Assertion cmetcusp1 
|- ( ( X =/= (/) /\ F e. CMetSp /\ U = ( metUnif ` D ) ) -> F e. CUnifSp )

Proof

Step Hyp Ref Expression
1 cmetcusp1.x 
 |-  X = ( Base ` F )
2 cmetcusp1.d 
 |-  D = ( ( dist ` F ) |` ( X X. X ) )
3 cmetcusp1.u 
 |-  U = ( UnifSt ` F )
4 cmsms 
 |-  ( F e. CMetSp -> F e. MetSp )
5 msxms 
 |-  ( F e. MetSp -> F e. *MetSp )
6 4 5 syl 
 |-  ( F e. CMetSp -> F e. *MetSp )
7 1 2 3 xmsusp 
 |-  ( ( X =/= (/) /\ F e. *MetSp /\ U = ( metUnif ` D ) ) -> F e. UnifSp )
8 6 7 syl3an2 
 |-  ( ( X =/= (/) /\ F e. CMetSp /\ U = ( metUnif ` D ) ) -> F e. UnifSp )
9 simpl3 
 |-  ( ( ( X =/= (/) /\ F e. CMetSp /\ U = ( metUnif ` D ) ) /\ c e. ( Fil ` X ) ) -> U = ( metUnif ` D ) )
10 9 fveq2d 
 |-  ( ( ( X =/= (/) /\ F e. CMetSp /\ U = ( metUnif ` D ) ) /\ c e. ( Fil ` X ) ) -> ( CauFilU ` U ) = ( CauFilU ` ( metUnif ` D ) ) )
11 10 eleq2d 
 |-  ( ( ( X =/= (/) /\ F e. CMetSp /\ U = ( metUnif ` D ) ) /\ c e. ( Fil ` X ) ) -> ( c e. ( CauFilU ` U ) <-> c e. ( CauFilU ` ( metUnif ` D ) ) ) )
12 simpl1 
 |-  ( ( ( X =/= (/) /\ F e. CMetSp /\ U = ( metUnif ` D ) ) /\ c e. ( Fil ` X ) ) -> X =/= (/) )
13 1 2 cmscmet 
 |-  ( F e. CMetSp -> D e. ( CMet ` X ) )
14 cmetmet 
 |-  ( D e. ( CMet ` X ) -> D e. ( Met ` X ) )
15 metxmet 
 |-  ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
16 13 14 15 3syl 
 |-  ( F e. CMetSp -> D e. ( *Met ` X ) )
17 16 3ad2ant2 
 |-  ( ( X =/= (/) /\ F e. CMetSp /\ U = ( metUnif ` D ) ) -> D e. ( *Met ` X ) )
18 17 adantr 
 |-  ( ( ( X =/= (/) /\ F e. CMetSp /\ U = ( metUnif ` D ) ) /\ c e. ( Fil ` X ) ) -> D e. ( *Met ` X ) )
19 simpr 
 |-  ( ( ( X =/= (/) /\ F e. CMetSp /\ U = ( metUnif ` D ) ) /\ c e. ( Fil ` X ) ) -> c e. ( Fil ` X ) )
20 cfilucfil4 
 |-  ( ( X =/= (/) /\ D e. ( *Met ` X ) /\ c e. ( Fil ` X ) ) -> ( c e. ( CauFilU ` ( metUnif ` D ) ) <-> c e. ( CauFil ` D ) ) )
21 12 18 19 20 syl3anc 
 |-  ( ( ( X =/= (/) /\ F e. CMetSp /\ U = ( metUnif ` D ) ) /\ c e. ( Fil ` X ) ) -> ( c e. ( CauFilU ` ( metUnif ` D ) ) <-> c e. ( CauFil ` D ) ) )
22 11 21 bitrd 
 |-  ( ( ( X =/= (/) /\ F e. CMetSp /\ U = ( metUnif ` D ) ) /\ c e. ( Fil ` X ) ) -> ( c e. ( CauFilU ` U ) <-> c e. ( CauFil ` D ) ) )
23 eqid 
 |-  ( MetOpen ` D ) = ( MetOpen ` D )
24 23 iscmet 
 |-  ( D e. ( CMet ` X ) <-> ( D e. ( Met ` X ) /\ A. c e. ( CauFil ` D ) ( ( MetOpen ` D ) fLim c ) =/= (/) ) )
25 24 simprbi 
 |-  ( D e. ( CMet ` X ) -> A. c e. ( CauFil ` D ) ( ( MetOpen ` D ) fLim c ) =/= (/) )
26 13 25 syl 
 |-  ( F e. CMetSp -> A. c e. ( CauFil ` D ) ( ( MetOpen ` D ) fLim c ) =/= (/) )
27 eqid 
 |-  ( TopOpen ` F ) = ( TopOpen ` F )
28 27 1 2 xmstopn 
 |-  ( F e. *MetSp -> ( TopOpen ` F ) = ( MetOpen ` D ) )
29 6 28 syl 
 |-  ( F e. CMetSp -> ( TopOpen ` F ) = ( MetOpen ` D ) )
30 29 oveq1d 
 |-  ( F e. CMetSp -> ( ( TopOpen ` F ) fLim c ) = ( ( MetOpen ` D ) fLim c ) )
31 30 neeq1d 
 |-  ( F e. CMetSp -> ( ( ( TopOpen ` F ) fLim c ) =/= (/) <-> ( ( MetOpen ` D ) fLim c ) =/= (/) ) )
32 31 ralbidv 
 |-  ( F e. CMetSp -> ( A. c e. ( CauFil ` D ) ( ( TopOpen ` F ) fLim c ) =/= (/) <-> A. c e. ( CauFil ` D ) ( ( MetOpen ` D ) fLim c ) =/= (/) ) )
33 26 32 mpbird 
 |-  ( F e. CMetSp -> A. c e. ( CauFil ` D ) ( ( TopOpen ` F ) fLim c ) =/= (/) )
34 33 r19.21bi 
 |-  ( ( F e. CMetSp /\ c e. ( CauFil ` D ) ) -> ( ( TopOpen ` F ) fLim c ) =/= (/) )
35 34 ex 
 |-  ( F e. CMetSp -> ( c e. ( CauFil ` D ) -> ( ( TopOpen ` F ) fLim c ) =/= (/) ) )
36 35 3ad2ant2 
 |-  ( ( X =/= (/) /\ F e. CMetSp /\ U = ( metUnif ` D ) ) -> ( c e. ( CauFil ` D ) -> ( ( TopOpen ` F ) fLim c ) =/= (/) ) )
37 36 adantr 
 |-  ( ( ( X =/= (/) /\ F e. CMetSp /\ U = ( metUnif ` D ) ) /\ c e. ( Fil ` X ) ) -> ( c e. ( CauFil ` D ) -> ( ( TopOpen ` F ) fLim c ) =/= (/) ) )
38 22 37 sylbid 
 |-  ( ( ( X =/= (/) /\ F e. CMetSp /\ U = ( metUnif ` D ) ) /\ c e. ( Fil ` X ) ) -> ( c e. ( CauFilU ` U ) -> ( ( TopOpen ` F ) fLim c ) =/= (/) ) )
39 38 ralrimiva 
 |-  ( ( X =/= (/) /\ F e. CMetSp /\ U = ( metUnif ` D ) ) -> A. c e. ( Fil ` X ) ( c e. ( CauFilU ` U ) -> ( ( TopOpen ` F ) fLim c ) =/= (/) ) )
40 1 3 27 iscusp2 
 |-  ( F e. CUnifSp <-> ( F e. UnifSp /\ A. c e. ( Fil ` X ) ( c e. ( CauFilU ` U ) -> ( ( TopOpen ` F ) fLim c ) =/= (/) ) ) )
41 8 39 40 sylanbrc 
 |-  ( ( X =/= (/) /\ F e. CMetSp /\ U = ( metUnif ` D ) ) -> F e. CUnifSp )