This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-bnd

Description: Define the class of bounded metrics. A metric space is bounded iff it can be covered by a single ball. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion df-bnd 
|- Bnd = ( x e. _V |-> { m e. ( Met ` x ) | A. y e. x E. r e. RR+ x = ( y ( ball ` m ) r ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cbnd 
 |-  Bnd
1 vx 
 |-  x
2 cvv 
 |-  _V
3 vm 
 |-  m
4 cmet 
 |-  Met
5 1 cv 
 |-  x
6 5 4 cfv 
 |-  ( Met ` x )
7 vy 
 |-  y
8 vr 
 |-  r
9 crp 
 |-  RR+
10 7 cv 
 |-  y
11 cbl 
 |-  ball
12 3 cv 
 |-  m
13 12 11 cfv 
 |-  ( ball ` m )
14 8 cv 
 |-  r
15 10 14 13 co 
 |-  ( y ( ball ` m ) r )
16 5 15 wceq 
 |-  x = ( y ( ball ` m ) r )
17 16 8 9 wrex 
 |-  E. r e. RR+ x = ( y ( ball ` m ) r )
18 17 7 5 wral 
 |-  A. y e. x E. r e. RR+ x = ( y ( ball ` m ) r )
19 18 3 6 crab 
 |-  { m e. ( Met ` x ) | A. y e. x E. r e. RR+ x = ( y ( ball ` m ) r ) }
20 1 2 19 cmpt 
 |-  ( x e. _V |-> { m e. ( Met ` x ) | A. y e. x E. r e. RR+ x = ( y ( ball ` m ) r ) } )
21 0 20 wceq 
 |-  Bnd = ( x e. _V |-> { m e. ( Met ` x ) | A. y e. x E. r e. RR+ x = ( y ( ball ` m ) r ) } )