Metamath Proof Explorer

Theorem metuel

Description: Elementhood in the uniform structure generated by a metric D (Contributed by Thierry Arnoux, 8-Dec-2017) (Revised by Thierry Arnoux, 11-Feb-2018)

Ref Expression
Assertion metuel 
|- ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( V e. ( metUnif ` D ) <-> ( V C_ ( X X. X ) /\ E. w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) w C_ V ) ) )

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 eleq2d 
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( V e. ( metUnif ` D ) <-> V e. ( ( X X. X ) filGen ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) ) ) )
4 oveq2 
 |-  ( a = e -> ( 0 [,) a ) = ( 0 [,) e ) )
5 4 imaeq2d 
 |-  ( a = e -> ( `' D " ( 0 [,) a ) ) = ( `' D " ( 0 [,) e ) ) )
6 5 cbvmptv 
 |-  ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) = ( e e. RR+ |-> ( `' D " ( 0 [,) e ) ) )
7 6 rneqi 
 |-  ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) = ran ( e e. RR+ |-> ( `' D " ( 0 [,) e ) ) )
8 7 metustfbas 
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) e. ( fBas ` ( X X. X ) ) )
9 elfg 
 |-  ( ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) e. ( fBas ` ( X X. X ) ) -> ( V e. ( ( X X. X ) filGen ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) ) <-> ( V C_ ( X X. X ) /\ E. w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) w C_ V ) ) )
10 8 9 syl 
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( V e. ( ( X X. X ) filGen ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) ) <-> ( V C_ ( X X. X ) /\ E. w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) w C_ V ) ) )
11 3 10 bitrd 
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( V e. ( metUnif ` D ) <-> ( V C_ ( X X. X ) /\ E. w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) w C_ V ) ) )