Metamath Proof Explorer

Theorem cfilucfil3

Description: Given a metric D and a uniform structure generated by that metric, Cauchy filter bases on that uniform structure are exactly the Cauchy filters for the metric. (Contributed by Thierry Arnoux, 15-Dec-2017) (Revised by Thierry Arnoux, 11-Feb-2018)

Ref Expression
Assertion cfilucfil3 
|- ( ( X =/= (/) /\ D e. ( *Met ` X ) ) -> ( ( C e. ( Fil ` X ) /\ C e. ( CauFilU ` ( metUnif ` D ) ) ) <-> C e. ( CauFil ` D ) ) )

Proof

Step Hyp Ref Expression
1 xmetpsmet 
 |-  ( D e. ( *Met ` X ) -> D e. ( PsMet ` X ) )
2 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 ) ) ) )
3 2 anbi2d 
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( ( C e. ( Fil ` X ) /\ C e. ( CauFilU ` ( metUnif ` D ) ) ) <-> ( C e. ( Fil ` X ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) ) )
4 filfbas 
 |-  ( C e. ( Fil ` X ) -> C e. ( fBas ` X ) )
5 4 pm4.71i 
 |-  ( C e. ( Fil ` X ) <-> ( C e. ( Fil ` X ) /\ C e. ( fBas ` X ) ) )
6 5 anbi1i 
 |-  ( ( C e. ( Fil ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) <-> ( ( C e. ( Fil ` X ) /\ C e. ( fBas ` X ) ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) )
7 anass 
 |-  ( ( ( C e. ( Fil ` X ) /\ C e. ( fBas ` X ) ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) <-> ( C e. ( Fil ` X ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) )
8 6 7 bitr2i 
 |-  ( ( C e. ( Fil ` X ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) <-> ( C e. ( Fil ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) )
9 3 8 bitrdi 
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( ( C e. ( Fil ` X ) /\ C e. ( CauFilU ` ( metUnif ` D ) ) ) <-> ( C e. ( Fil ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) )
10 1 9 sylan2 
 |-  ( ( X =/= (/) /\ D e. ( *Met ` X ) ) -> ( ( C e. ( Fil ` X ) /\ C e. ( CauFilU ` ( metUnif ` D ) ) ) <-> ( C e. ( Fil ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) )
11 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 ) ) ) )
12 11 adantl 
 |-  ( ( X =/= (/) /\ 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 ) ) ) )
13 10 12 bitr4d 
 |-  ( ( X =/= (/) /\ D e. ( *Met ` X ) ) -> ( ( C e. ( Fil ` X ) /\ C e. ( CauFilU ` ( metUnif ` D ) ) ) <-> C e. ( CauFil ` D ) ) )