Metamath Proof Explorer

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 ∈ V ⟼ m ∈ Met ⁡ x | ∀ y ∈ x ∃ r ∈ ℝ + 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 ∃ r ∈ ℝ + x = y ball ⁡ m r
18 17 7 5 wral wff ∀ y ∈ x ∃ r ∈ ℝ + x = y ball ⁡ m r
19 18 3 6 crab class m ∈ Met ⁡ x | ∀ y ∈ x ∃ r ∈ ℝ + x = y ball ⁡ m r
20 1 2 19 cmpt class x ∈ V ⟼ m ∈ Met ⁡ x | ∀ y ∈ x ∃ r ∈ ℝ + x = y ball ⁡ m r
21 0 20 wceq wff Bnd = x ∈ V ⟼ m ∈ Met ⁡ x | ∀ y ∈ x ∃ r ∈ ℝ + x = y ball ⁡ m r