Step |
Hyp |
Ref |
Expression |
1 |
|
elfvex |
|- ( M e. ( Bnd ` X ) -> X e. _V ) |
2 |
|
elfvex |
|- ( M e. ( Met ` X ) -> X e. _V ) |
3 |
2
|
adantr |
|- ( ( M e. ( Met ` X ) /\ A. x e. X E. r e. RR+ X = ( x ( ball ` M ) r ) ) -> X e. _V ) |
4 |
|
fveq2 |
|- ( y = X -> ( Met ` y ) = ( Met ` X ) ) |
5 |
|
eqeq1 |
|- ( y = X -> ( y = ( x ( ball ` m ) r ) <-> X = ( x ( ball ` m ) r ) ) ) |
6 |
5
|
rexbidv |
|- ( y = X -> ( E. r e. RR+ y = ( x ( ball ` m ) r ) <-> E. r e. RR+ X = ( x ( ball ` m ) r ) ) ) |
7 |
6
|
raleqbi1dv |
|- ( y = X -> ( A. x e. y E. r e. RR+ y = ( x ( ball ` m ) r ) <-> A. x e. X E. r e. RR+ X = ( x ( ball ` m ) r ) ) ) |
8 |
4 7
|
rabeqbidv |
|- ( y = X -> { m e. ( Met ` y ) | A. x e. y E. r e. RR+ y = ( x ( ball ` m ) r ) } = { m e. ( Met ` X ) | A. x e. X E. r e. RR+ X = ( x ( ball ` m ) r ) } ) |
9 |
|
df-bnd |
|- Bnd = ( y e. _V |-> { m e. ( Met ` y ) | A. x e. y E. r e. RR+ y = ( x ( ball ` m ) r ) } ) |
10 |
|
fvex |
|- ( Met ` X ) e. _V |
11 |
10
|
rabex |
|- { m e. ( Met ` X ) | A. x e. X E. r e. RR+ X = ( x ( ball ` m ) r ) } e. _V |
12 |
8 9 11
|
fvmpt |
|- ( X e. _V -> ( Bnd ` X ) = { m e. ( Met ` X ) | A. x e. X E. r e. RR+ X = ( x ( ball ` m ) r ) } ) |
13 |
12
|
eleq2d |
|- ( X e. _V -> ( M e. ( Bnd ` X ) <-> M e. { m e. ( Met ` X ) | A. x e. X E. r e. RR+ X = ( x ( ball ` m ) r ) } ) ) |
14 |
|
fveq2 |
|- ( m = M -> ( ball ` m ) = ( ball ` M ) ) |
15 |
14
|
oveqd |
|- ( m = M -> ( x ( ball ` m ) r ) = ( x ( ball ` M ) r ) ) |
16 |
15
|
eqeq2d |
|- ( m = M -> ( X = ( x ( ball ` m ) r ) <-> X = ( x ( ball ` M ) r ) ) ) |
17 |
16
|
rexbidv |
|- ( m = M -> ( E. r e. RR+ X = ( x ( ball ` m ) r ) <-> E. r e. RR+ X = ( x ( ball ` M ) r ) ) ) |
18 |
17
|
ralbidv |
|- ( m = M -> ( A. x e. X E. r e. RR+ X = ( x ( ball ` m ) r ) <-> A. x e. X E. r e. RR+ X = ( x ( ball ` M ) r ) ) ) |
19 |
18
|
elrab |
|- ( M e. { m e. ( Met ` X ) | A. x e. X E. r e. RR+ X = ( x ( ball ` m ) r ) } <-> ( M e. ( Met ` X ) /\ A. x e. X E. r e. RR+ X = ( x ( ball ` M ) r ) ) ) |
20 |
13 19
|
syl6bb |
|- ( X e. _V -> ( M e. ( Bnd ` X ) <-> ( M e. ( Met ` X ) /\ A. x e. X E. r e. RR+ X = ( x ( ball ` M ) r ) ) ) ) |
21 |
1 3 20
|
pm5.21nii |
|- ( M e. ( Bnd ` X ) <-> ( M e. ( Met ` X ) /\ A. x e. X E. r e. RR+ X = ( x ( ball ` M ) r ) ) ) |