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 ) ) ) ) |