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