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