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 e. ( CMet ` X ) ) -> ( toUnifSp ` ( metUnif ` D ) ) e. CUnifSp )

Proof

Step Hyp Ref Expression
1 cmetmet 
 |-  ( D e. ( CMet ` X ) -> D e. ( Met ` X ) )
2 metxmet 
 |-  ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
3 xmetpsmet 
 |-  ( D e. ( *Met ` X ) -> D e. ( PsMet ` X ) )
4 1 2 3 3syl 
 |-  ( D e. ( CMet ` X ) -> D e. ( PsMet ` X ) )
5 4 anim2i 
 |-  ( ( X =/= (/) /\ D e. ( CMet ` X ) ) -> ( X =/= (/) /\ D e. ( PsMet ` X ) ) )
6 metuust 
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( metUnif ` D ) e. ( UnifOn ` X ) )
7 eqid 
 |-  ( toUnifSp ` ( metUnif ` D ) ) = ( toUnifSp ` ( metUnif ` D ) )
8 7 tususp 
 |-  ( ( metUnif ` D ) e. ( UnifOn ` X ) -> ( toUnifSp ` ( metUnif ` D ) ) e. UnifSp )
9 5 6 8 3syl 
 |-  ( ( X =/= (/) /\ D e. ( CMet ` X ) ) -> ( toUnifSp ` ( metUnif ` D ) ) e. UnifSp )
10 simpll 
 |-  ( ( ( ( X =/= (/) /\ D e. ( CMet ` X ) ) /\ c e. ( Fil ` ( Base ` ( toUnifSp ` ( metUnif ` D ) ) ) ) ) /\ c e. ( CauFilU ` ( UnifSt ` ( toUnifSp ` ( metUnif ` D ) ) ) ) ) -> ( X =/= (/) /\ D e. ( CMet ` X ) ) )
11 10 simprd 
 |-  ( ( ( ( X =/= (/) /\ D e. ( CMet ` X ) ) /\ c e. ( Fil ` ( Base ` ( toUnifSp ` ( metUnif ` D ) ) ) ) ) /\ c e. ( CauFilU ` ( UnifSt ` ( toUnifSp ` ( metUnif ` D ) ) ) ) ) -> D e. ( CMet ` X ) )
12 1 2 syl 
 |-  ( D e. ( CMet ` X ) -> D e. ( *Met ` X ) )
13 12 ad3antlr 
 |-  ( ( ( ( X =/= (/) /\ D e. ( CMet ` X ) ) /\ c e. ( Fil ` ( Base ` ( toUnifSp ` ( metUnif ` D ) ) ) ) ) /\ c e. ( CauFilU ` ( UnifSt ` ( toUnifSp ` ( metUnif ` D ) ) ) ) ) -> D e. ( *Met ` X ) )
14 7 tusbas 
 |-  ( ( metUnif ` D ) e. ( UnifOn ` X ) -> X = ( Base ` ( toUnifSp ` ( metUnif ` D ) ) ) )
15 14 fveq2d 
 |-  ( ( metUnif ` D ) e. ( UnifOn ` X ) -> ( Fil ` X ) = ( Fil ` ( Base ` ( toUnifSp ` ( metUnif ` D ) ) ) ) )
16 15 eleq2d 
 |-  ( ( metUnif ` D ) e. ( UnifOn ` X ) -> ( c e. ( Fil ` X ) <-> c e. ( Fil ` ( Base ` ( toUnifSp ` ( metUnif ` D ) ) ) ) ) )
17 5 6 16 3syl 
 |-  ( ( X =/= (/) /\ D e. ( CMet ` X ) ) -> ( c e. ( Fil ` X ) <-> c e. ( Fil ` ( Base ` ( toUnifSp ` ( metUnif ` D ) ) ) ) ) )
18 17 biimpar 
 |-  ( ( ( X =/= (/) /\ D e. ( CMet ` X ) ) /\ c e. ( Fil ` ( Base ` ( toUnifSp ` ( metUnif ` D ) ) ) ) ) -> c e. ( Fil ` X ) )
19 18 adantr 
 |-  ( ( ( ( X =/= (/) /\ D e. ( CMet ` X ) ) /\ c e. ( Fil ` ( Base ` ( toUnifSp ` ( metUnif ` D ) ) ) ) ) /\ c e. ( CauFilU ` ( UnifSt ` ( toUnifSp ` ( metUnif ` D ) ) ) ) ) -> c e. ( Fil ` X ) )
20 7 tususs 
 |-  ( ( metUnif ` D ) e. ( UnifOn ` X ) -> ( metUnif ` D ) = ( UnifSt ` ( toUnifSp ` ( metUnif ` D ) ) ) )
21 20 fveq2d 
 |-  ( ( metUnif ` D ) e. ( UnifOn ` X ) -> ( CauFilU ` ( metUnif ` D ) ) = ( CauFilU ` ( UnifSt ` ( toUnifSp ` ( metUnif ` D ) ) ) ) )
22 5 6 21 3syl 
 |-  ( ( X =/= (/) /\ D e. ( CMet ` X ) ) -> ( CauFilU ` ( metUnif ` D ) ) = ( CauFilU ` ( UnifSt ` ( toUnifSp ` ( metUnif ` D ) ) ) ) )
23 22 eleq2d 
 |-  ( ( X =/= (/) /\ D e. ( CMet ` X ) ) -> ( c e. ( CauFilU ` ( metUnif ` D ) ) <-> c e. ( CauFilU ` ( UnifSt ` ( toUnifSp ` ( metUnif ` D ) ) ) ) ) )
24 23 biimpar 
 |-  ( ( ( X =/= (/) /\ D e. ( CMet ` X ) ) /\ c e. ( CauFilU ` ( UnifSt ` ( toUnifSp ` ( metUnif ` D ) ) ) ) ) -> c e. ( CauFilU ` ( metUnif ` D ) ) )
25 24 adantlr 
 |-  ( ( ( ( X =/= (/) /\ D e. ( CMet ` X ) ) /\ c e. ( Fil ` ( Base ` ( toUnifSp ` ( metUnif ` D ) ) ) ) ) /\ c e. ( CauFilU ` ( UnifSt ` ( toUnifSp ` ( metUnif ` D ) ) ) ) ) -> c e. ( CauFilU ` ( metUnif ` D ) ) )
26 cfilucfil2 
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( c e. ( CauFilU ` ( metUnif ` D ) ) <-> ( c e. ( fBas ` X ) /\ A. x e. RR+ E. y e. c ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) )
27 5 26 syl 
 |-  ( ( X =/= (/) /\ D e. ( CMet ` X ) ) -> ( c e. ( CauFilU ` ( metUnif ` D ) ) <-> ( c e. ( fBas ` X ) /\ A. x e. RR+ E. y e. c ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) )
28 27 simplbda 
 |-  ( ( ( X =/= (/) /\ D e. ( CMet ` X ) ) /\ c e. ( CauFilU ` ( metUnif ` D ) ) ) -> A. x e. RR+ E. y e. c ( D " ( y X. y ) ) C_ ( 0 [,) x ) )
29 10 25 28 syl2anc 
 |-  ( ( ( ( X =/= (/) /\ D e. ( CMet ` X ) ) /\ c e. ( Fil ` ( Base ` ( toUnifSp ` ( metUnif ` D ) ) ) ) ) /\ c e. ( CauFilU ` ( UnifSt ` ( toUnifSp ` ( metUnif ` D ) ) ) ) ) -> A. x e. RR+ E. y e. c ( D " ( y X. y ) ) C_ ( 0 [,) x ) )
30 iscfil 
 |-  ( D e. ( *Met ` X ) -> ( c e. ( CauFil ` D ) <-> ( c e. ( Fil ` X ) /\ A. x e. RR+ E. y e. c ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) )
31 30 biimpar 
 |-  ( ( D e. ( *Met ` X ) /\ ( c e. ( Fil ` X ) /\ A. x e. RR+ E. y e. c ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) -> c e. ( CauFil ` D ) )
32 13 19 29 31 syl12anc 
 |-  ( ( ( ( X =/= (/) /\ D e. ( CMet ` X ) ) /\ c e. ( Fil ` ( Base ` ( toUnifSp ` ( metUnif ` D ) ) ) ) ) /\ c e. ( CauFilU ` ( UnifSt ` ( toUnifSp ` ( metUnif ` D ) ) ) ) ) -> c e. ( CauFil ` D ) )
33 eqid 
 |-  ( MetOpen ` D ) = ( MetOpen ` D )
34 33 cmetcvg 
 |-  ( ( D e. ( CMet ` X ) /\ c e. ( CauFil ` D ) ) -> ( ( MetOpen ` D ) fLim c ) =/= (/) )
35 11 32 34 syl2anc 
 |-  ( ( ( ( X =/= (/) /\ D e. ( CMet ` X ) ) /\ c e. ( Fil ` ( Base ` ( toUnifSp ` ( metUnif ` D ) ) ) ) ) /\ c e. ( CauFilU ` ( UnifSt ` ( toUnifSp ` ( metUnif ` D ) ) ) ) ) -> ( ( MetOpen ` D ) fLim c ) =/= (/) )
36 eqid 
 |-  ( unifTop ` ( metUnif ` D ) ) = ( unifTop ` ( metUnif ` D ) )
37 7 36 tustopn 
 |-  ( ( metUnif ` D ) e. ( UnifOn ` X ) -> ( unifTop ` ( metUnif ` D ) ) = ( TopOpen ` ( toUnifSp ` ( metUnif ` D ) ) ) )
38 5 6 37 3syl 
 |-  ( ( X =/= (/) /\ D e. ( CMet ` X ) ) -> ( unifTop ` ( metUnif ` D ) ) = ( TopOpen ` ( toUnifSp ` ( metUnif ` D ) ) ) )
39 12 anim2i 
 |-  ( ( X =/= (/) /\ D e. ( CMet ` X ) ) -> ( X =/= (/) /\ D e. ( *Met ` X ) ) )
40 xmetutop 
 |-  ( ( X =/= (/) /\ D e. ( *Met ` X ) ) -> ( unifTop ` ( metUnif ` D ) ) = ( MetOpen ` D ) )
41 39 40 syl 
 |-  ( ( X =/= (/) /\ D e. ( CMet ` X ) ) -> ( unifTop ` ( metUnif ` D ) ) = ( MetOpen ` D ) )
42 38 41 eqtr3d 
 |-  ( ( X =/= (/) /\ D e. ( CMet ` X ) ) -> ( TopOpen ` ( toUnifSp ` ( metUnif ` D ) ) ) = ( MetOpen ` D ) )
43 42 oveq1d 
 |-  ( ( X =/= (/) /\ D e. ( CMet ` X ) ) -> ( ( TopOpen ` ( toUnifSp ` ( metUnif ` D ) ) ) fLim c ) = ( ( MetOpen ` D ) fLim c ) )
44 43 neeq1d 
 |-  ( ( X =/= (/) /\ D e. ( CMet ` X ) ) -> ( ( ( TopOpen ` ( toUnifSp ` ( metUnif ` D ) ) ) fLim c ) =/= (/) <-> ( ( MetOpen ` D ) fLim c ) =/= (/) ) )
45 44 biimpar 
 |-  ( ( ( X =/= (/) /\ D e. ( CMet ` X ) ) /\ ( ( MetOpen ` D ) fLim c ) =/= (/) ) -> ( ( TopOpen ` ( toUnifSp ` ( metUnif ` D ) ) ) fLim c ) =/= (/) )
46 10 35 45 syl2anc 
 |-  ( ( ( ( X =/= (/) /\ D e. ( CMet ` X ) ) /\ c e. ( Fil ` ( Base ` ( toUnifSp ` ( metUnif ` D ) ) ) ) ) /\ c e. ( CauFilU ` ( UnifSt ` ( toUnifSp ` ( metUnif ` D ) ) ) ) ) -> ( ( TopOpen ` ( toUnifSp ` ( metUnif ` D ) ) ) fLim c ) =/= (/) )
47 46 ex 
 |-  ( ( ( X =/= (/) /\ D e. ( CMet ` X ) ) /\ c e. ( Fil ` ( Base ` ( toUnifSp ` ( metUnif ` D ) ) ) ) ) -> ( c e. ( CauFilU ` ( UnifSt ` ( toUnifSp ` ( metUnif ` D ) ) ) ) -> ( ( TopOpen ` ( toUnifSp ` ( metUnif ` D ) ) ) fLim c ) =/= (/) ) )
48 47 ralrimiva 
 |-  ( ( X =/= (/) /\ D e. ( CMet ` X ) ) -> A. c e. ( Fil ` ( Base ` ( toUnifSp ` ( metUnif ` D ) ) ) ) ( c e. ( CauFilU ` ( UnifSt ` ( toUnifSp ` ( metUnif ` D ) ) ) ) -> ( ( TopOpen ` ( toUnifSp ` ( metUnif ` D ) ) ) fLim c ) =/= (/) ) )
49 iscusp 
 |-  ( ( toUnifSp ` ( metUnif ` D ) ) e. CUnifSp <-> ( ( toUnifSp ` ( metUnif ` D ) ) e. UnifSp /\ A. c e. ( Fil ` ( Base ` ( toUnifSp ` ( metUnif ` D ) ) ) ) ( c e. ( CauFilU ` ( UnifSt ` ( toUnifSp ` ( metUnif ` D ) ) ) ) -> ( ( TopOpen ` ( toUnifSp ` ( metUnif ` D ) ) ) fLim c ) =/= (/) ) ) )
50 9 48 49 sylanbrc 
 |-  ( ( X =/= (/) /\ D e. ( CMet ` X ) ) -> ( toUnifSp ` ( metUnif ` D ) ) e. CUnifSp )