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 \in V ⟼ \{m \in Met (x) \| \forall y \in x \exists r \in ℝ^{+} x = y ball (m) r\})$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cbnd	$class Bnd$
1		vx	$setvar x$
2		cvv	$class V$
3		vm	$setvar m$
4		cmet	$class Met$
5	1	cv	$setvar x$
6	5 4	cfv	$class Met (x)$
7		vy	$setvar y$
8		vr	$setvar r$
9		crp	$class ℝ^{+}$
10	7	cv	$setvar y$
11		cbl	$class ball$
12	3	cv	$setvar m$
13	12 11	cfv	$class ball (m)$
14	8	cv	$setvar r$
15	10 14 13	co	$class (y ball (m) r)$
16	5 15	wceq	$wff x = y ball (m) r$
17	16 8 9	wrex	$wff \exists r \in ℝ^{+} x = y ball (m) r$
18	17 7 5	wral	$wff \forall y \in x \exists r \in ℝ^{+} x = y ball (m) r$
19	18 3 6	crab	$class \{m \in Met (x) \| \forall y \in x \exists r \in ℝ^{+} x = y ball (m) r\}$
20	1 2 19	cmpt	$class (x \in V ⟼ \{m \in Met (x) \| \forall y \in x \exists r \in ℝ^{+} x = y ball (m) r\})$
21	0 20	wceq	$wff Bnd = (x \in V ⟼ \{m \in Met (x) \| \forall y \in x \exists r \in ℝ^{+} x = y ball (m) r\})$

Metamath Proof Explorer

Definition df-bnd

Detailed syntax breakdown