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 syl5bb
 |-  ( D e. ( PsMet ` X ) -> ( B e. F <-> E. a e. RR+ B = ( `' D " ( 0 [,) a ) ) ) )