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