Metamath Proof Explorer

Theorem isbnd

Description: The predicate "is a bounded metric space". (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 12-Sep-2015)

Ref Expression
Assertion isbnd 
|- ( M e. ( Bnd ` X ) <-> ( M e. ( Met ` X ) /\ A. x e. X E. r e. RR+ X = ( x ( ball ` M ) r ) ) )

Proof

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