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

Metamath Proof Explorer

Definition df-totbnd

Description: Define the class of totally bounded metrics. A metric space is totally bounded iff it can be covered by a finite number of balls of any given radius. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion df-totbnd 
|- TotBnd = ( x e. _V |-> { m e. ( Met ` x ) | A. d e. RR+ E. v e. Fin ( U. v = x /\ A. b e. v E. y e. x b = ( y ( ball ` m ) d ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctotbnd 
 |-  TotBnd
1 vx 
 |-  x
2 cvv 
 |-  _V
3 vm 
 |-  m
4 cmet 
 |-  Met
5 1 cv 
 |-  x
6 5 4 cfv 
 |-  ( Met ` x )
7 vd 
 |-  d
8 crp 
 |-  RR+
9 vv 
 |-  v
10 cfn 
 |-  Fin
11 9 cv 
 |-  v
12 11 cuni 
 |-  U. v
13 12 5 wceq 
 |-  U. v = x
14 vb 
 |-  b
15 vy 
 |-  y
16 14 cv 
 |-  b
17 15 cv 
 |-  y
18 cbl 
 |-  ball
19 3 cv 
 |-  m
20 19 18 cfv 
 |-  ( ball ` m )
21 7 cv 
 |-  d
22 17 21 20 co 
 |-  ( y ( ball ` m ) d )
23 16 22 wceq 
 |-  b = ( y ( ball ` m ) d )
24 23 15 5 wrex 
 |-  E. y e. x b = ( y ( ball ` m ) d )
25 24 14 11 wral 
 |-  A. b e. v E. y e. x b = ( y ( ball ` m ) d )
26 13 25 wa 
 |-  ( U. v = x /\ A. b e. v E. y e. x b = ( y ( ball ` m ) d ) )
27 26 9 10 wrex 
 |-  E. v e. Fin ( U. v = x /\ A. b e. v E. y e. x b = ( y ( ball ` m ) d ) )
28 27 7 8 wral 
 |-  A. d e. RR+ E. v e. Fin ( U. v = x /\ A. b e. v E. y e. x b = ( y ( ball ` m ) d ) )
29 28 3 6 crab 
 |-  { m e. ( Met ` x ) | A. d e. RR+ E. v e. Fin ( U. v = x /\ A. b e. v E. y e. x b = ( y ( ball ` m ) d ) ) }
30 1 2 29 cmpt 
 |-  ( x e. _V |-> { m e. ( Met ` x ) | A. d e. RR+ E. v e. Fin ( U. v = x /\ A. b e. v E. y e. x b = ( y ( ball ` m ) d ) ) } )
31 0 30 wceq 
 |-  TotBnd = ( x e. _V |-> { m e. ( Met ` x ) | A. d e. RR+ E. v e. Fin ( U. v = x /\ A. b e. v E. y e. x b = ( y ( ball ` m ) d ) ) } )