Metamath Proof Explorer

Theorem cfilucfil2

Description: Given a metric D and a uniform structure generated by that metric, Cauchy filter bases on that uniform structure are exactly the filter bases which contain balls of any pre-chosen size. See iscfil . (Contributed by Thierry Arnoux, 1-Dec-2017) (Revised by Thierry Arnoux, 11-Feb-2018)

Ref Expression
Assertion 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 ) ) ) )

Proof

Step Hyp Ref Expression
1 metuval 
 |-  ( D e. ( PsMet ` X ) -> ( metUnif ` D ) = ( ( X X. X ) filGen ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) ) )
2 1 adantl 
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( metUnif ` D ) = ( ( X X. X ) filGen ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) ) )
3 2 fveq2d 
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( CauFilU ` ( metUnif ` D ) ) = ( CauFilU ` ( ( X X. X ) filGen ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) ) ) )
4 3 eleq2d 
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( C e. ( CauFilU ` ( metUnif ` D ) ) <-> C e. ( CauFilU ` ( ( X X. X ) filGen ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) ) ) ) )
5 oveq2 
 |-  ( a = b -> ( 0 [,) a ) = ( 0 [,) b ) )
6 5 imaeq2d 
 |-  ( a = b -> ( `' D " ( 0 [,) a ) ) = ( `' D " ( 0 [,) b ) ) )
7 6 cbvmptv 
 |-  ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) = ( b e. RR+ |-> ( `' D " ( 0 [,) b ) ) )
8 7 rneqi 
 |-  ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) = ran ( b e. RR+ |-> ( `' D " ( 0 [,) b ) ) )
9 8 cfilucfil 
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( C e. ( CauFilU ` ( ( X X. X ) filGen ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) ) ) <-> ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) )
10 4 9 bitrd 
 |-  ( ( 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 ) ) ) )