This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem metustel

Description: Define a filter base F generated by a metric D . (Contributed by Thierry Arnoux, 22-Nov-2017) (Revised by Thierry Arnoux, 11-Feb-2018)

Ref Expression
Hypothesis metust.1 
|- F = ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )
Assertion metustel 
|- ( D e. ( PsMet ` X ) -> ( B e. F <-> E. a e. RR+ B = ( `' D " ( 0 [,) a ) ) ) )

Proof

Step Hyp Ref Expression
1 metust.1 
 |-  F = ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )
2 1 eleq2i 
 |-  ( B e. F <-> B e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) )
3 elex 
 |-  ( B e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) -> B e. _V )
4 3 a1i 
 |-  ( D e. ( PsMet ` X ) -> ( B e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) -> B e. _V ) )
5 cnvexg 
 |-  ( D e. ( PsMet ` X ) -> `' D e. _V )
6 imaexg 
 |-  ( `' D e. _V -> ( `' D " ( 0 [,) a ) ) e. _V )
7 eleq1a 
 |-  ( ( `' D " ( 0 [,) a ) ) e. _V -> ( B = ( `' D " ( 0 [,) a ) ) -> B e. _V ) )
8 5 6 7 3syl 
 |-  ( D e. ( PsMet ` X ) -> ( B = ( `' D " ( 0 [,) a ) ) -> B e. _V ) )
9 8 rexlimdvw 
 |-  ( D e. ( PsMet ` X ) -> ( E. a e. RR+ B = ( `' D " ( 0 [,) a ) ) -> B e. _V ) )
10 eqid 
 |-  ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) = ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )
11 10 elrnmpt 
 |-  ( B e. _V -> ( B e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) <-> E. a e. RR+ B = ( `' D " ( 0 [,) a ) ) ) )
12 11 a1i 
 |-  ( D e. ( PsMet ` X ) -> ( B e. _V -> ( B e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) <-> E. a e. RR+ B = ( `' D " ( 0 [,) a ) ) ) ) )
13 4 9 12 pm5.21ndd 
 |-  ( D e. ( PsMet ` X ) -> ( B e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) <-> E. a e. RR+ B = ( `' D " ( 0 [,) a ) ) ) )
14 2 13 bitrid 
 |-  ( D e. ( PsMet ` X ) -> ( B e. F <-> E. a e. RR+ B = ( `' D " ( 0 [,) a ) ) ) )