Definition df-bnd 33578

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

Assertion

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

Distinct variable group:   m, r, x, y

Detailed syntax breakdown of Definition df-bnd

Step	Hyp	Ref	Expression
1		cbnd 33566	. 2 class Bnd
2		vx	. . 3 setvar x
3		cvv 3200	. . 3 class _V
4	2	cv 1482	. . . . . . 7 class x
5		vy	. . . . . . . . 9 setvar y
6	5	cv 1482	. . . . . . . 8 class y
7		vr	. . . . . . . . 9 setvar r
8	7	cv 1482	. . . . . . . 8 class r
9		vm	. . . . . . . . . 10 setvar m
10	9	cv 1482	. . . . . . . . 9 class m
11		cbl 19733	. . . . . . . . 9 class ball
12	10, 11	cfv 5888	. . . . . . . 8 class ( ball ` m )
13	6, 8, 12	co 6650	. . . . . . 7 class ( y ( ball ` m ) r )
14	4, 13	wceq 1483	. . . . . 6 wff x = ( y ( ball ` m ) r )
15		crp 11832	. . . . . 6 class RR+
16	14, 7, 15	wrex 2913	. . . . 5 wff E. r e. RR+ x = ( y ( ball ` m ) r )
17	16, 5, 4	wral 2912	. . . 4 wff A. y e. x E. r e. RR+ x = ( y ( ball ` m ) r )
18		cme 19732	. . . . 5 class Met
19	4, 18	cfv 5888	. . . 4 class ( Met ` x )
20	17, 9, 19	crab 2916	. . 3 class { m e. ( Met ` x ) | A. y e. x E. r e. RR+ x = ( y ( ball ` m ) r ) }
21	2, 3, 20	cmpt 4729	. 2 class ( x e. _V |-> { m e. ( Met ` x ) | A. y e. x E. r e. RR+ x = ( y ( ball ` m ) r ) } )
22	1, 21	wceq 1483	1 wff Bnd = ( x e. _V |-> { m e. ( Met ` x ) | A. y e. x E. r e. RR+ x = ( y ( ball ` m ) r ) } )

This definition is referenced by:  isbnd  33579