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