Metamath Proof Explorer

Theorem cfilucfil4

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 cfilucfil4 
|- ( ( X =/= (/) /\ D e. ( *Met ` X ) /\ C e. ( Fil ` X ) ) -> ( C e. ( CauFilU ` ( metUnif ` D ) ) <-> C e. ( CauFil ` D ) ) )

Proof

Step Hyp Ref Expression
1 cfilucfil3 
 |-  ( ( X =/= (/) /\ D e. ( *Met ` X ) ) -> ( ( C e. ( Fil ` X ) /\ C e. ( CauFilU ` ( metUnif ` D ) ) ) <-> C e. ( CauFil ` D ) ) )
2 cfilfil 
 |-  ( ( D e. ( *Met ` X ) /\ C e. ( CauFil ` D ) ) -> C e. ( Fil ` X ) )
3 2 ex 
 |-  ( D e. ( *Met ` X ) -> ( C e. ( CauFil ` D ) -> C e. ( Fil ` X ) ) )
4 3 adantl 
 |-  ( ( X =/= (/) /\ D e. ( *Met ` X ) ) -> ( C e. ( CauFil ` D ) -> C e. ( Fil ` X ) ) )
5 4 pm4.71rd 
 |-  ( ( X =/= (/) /\ D e. ( *Met ` X ) ) -> ( C e. ( CauFil ` D ) <-> ( C e. ( Fil ` X ) /\ C e. ( CauFil ` D ) ) ) )
6 1 5 bitrd 
 |-  ( ( X =/= (/) /\ D e. ( *Met ` X ) ) -> ( ( C e. ( Fil ` X ) /\ C e. ( CauFilU ` ( metUnif ` D ) ) ) <-> ( C e. ( Fil ` X ) /\ C e. ( CauFil ` D ) ) ) )
7 pm5.32 
 |-  ( ( C e. ( Fil ` X ) -> ( C e. ( CauFilU ` ( metUnif ` D ) ) <-> C e. ( CauFil ` D ) ) ) <-> ( ( C e. ( Fil ` X ) /\ C e. ( CauFilU ` ( metUnif ` D ) ) ) <-> ( C e. ( Fil ` X ) /\ C e. ( CauFil ` D ) ) ) )
8 6 7 sylibr 
 |-  ( ( X =/= (/) /\ D e. ( *Met ` X ) ) -> ( C e. ( Fil ` X ) -> ( C e. ( CauFilU ` ( metUnif ` D ) ) <-> C e. ( CauFil ` D ) ) ) )
9 8 3impia 
 |-  ( ( X =/= (/) /\ D e. ( *Met ` X ) /\ C e. ( Fil ` X ) ) -> ( C e. ( CauFilU ` ( metUnif ` D ) ) <-> C e. ( CauFil ` D ) ) )