Definition df-totbnd 33567

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

Assertion

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

Distinct variable group:   b, d, m, v, x, y

Detailed syntax breakdown of Definition df-totbnd

Step	Hyp	Ref	Expression
1		ctotbnd 33565	. 2 class TotBnd
2		vx	. . 3 setvar x
3		cvv 3200	. . 3 class _V
4		vv	. . . . . . . . . 10 setvar v
5	4	cv 1482	. . . . . . . . 9 class v
6	5	cuni 4436	. . . . . . . 8 class U. v
7	2	cv 1482	. . . . . . . 8 class x
8	6, 7	wceq 1483	. . . . . . 7 wff U. v = x
9		vb	. . . . . . . . . . 11 setvar b
10	9	cv 1482	. . . . . . . . . 10 class b
11		vy	. . . . . . . . . . . 12 setvar y
12	11	cv 1482	. . . . . . . . . . 11 class y
13		vd	. . . . . . . . . . . 12 setvar d
14	13	cv 1482	. . . . . . . . . . 11 class d
15		vm	. . . . . . . . . . . . 13 setvar m
16	15	cv 1482	. . . . . . . . . . . 12 class m
17		cbl 19733	. . . . . . . . . . . 12 class ball
18	16, 17	cfv 5888	. . . . . . . . . . 11 class ( ball ` m )
19	12, 14, 18	co 6650	. . . . . . . . . 10 class ( y ( ball ` m ) d )
20	10, 19	wceq 1483	. . . . . . . . 9 wff b = ( y ( ball ` m ) d )
21	20, 11, 7	wrex 2913	. . . . . . . 8 wff E. y e. x b = ( y ( ball ` m ) d )
22	21, 9, 5	wral 2912	. . . . . . 7 wff A. b e. v E. y e. x b = ( y ( ball ` m ) d )
23	8, 22	wa 384	. . . . . 6 wff ( U. v = x /\ A. b e. v E. y e. x b = ( y ( ball ` m ) d ) )
24		cfn 7955	. . . . . 6 class Fin
25	23, 4, 24	wrex 2913	. . . . 5 wff E. v e. Fin ( U. v = x /\ A. b e. v E. y e. x b = ( y ( ball ` m ) d ) )
26		crp 11832	. . . . 5 class RR+
27	25, 13, 26	wral 2912	. . . 4 wff A. d e. RR+ E. v e. Fin ( U. v = x /\ A. b e. v E. y e. x b = ( y ( ball ` m ) d ) )
28		cme 19732	. . . . 5 class Met
29	7, 28	cfv 5888	. . . 4 class ( Met ` x )
30	27, 15, 29	crab 2916	. . 3 class { 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	2, 3, 30	cmpt 4729	. 2 class ( 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 ) ) } )
32	1, 31	wceq 1483	1 wff 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 ) ) } )

This definition is referenced by:  istotbnd  33568