Definition df-bnd 35864

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 = (𝑥 ∈ V ↦ {𝑚 ∈ (Met‘𝑥) ∣ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑥 = (𝑦(ball‘𝑚)𝑟)})

Distinct variable group:   𝑚,𝑟,𝑥,𝑦

Detailed syntax breakdown of Definition df-bnd

Step	Hyp	Ref	Expression
1		cbnd 35852	. 2 class Bnd
2		vx	. . 3 setvar 𝑥
3		cvv 3422	. . 3 class V
4	2	cv 1538	. . . . . . 7 class 𝑥
5		vy	. . . . . . . . 9 setvar 𝑦
6	5	cv 1538	. . . . . . . 8 class 𝑦
7		vr	. . . . . . . . 9 setvar 𝑟
8	7	cv 1538	. . . . . . . 8 class 𝑟
9		vm	. . . . . . . . . 10 setvar 𝑚
10	9	cv 1538	. . . . . . . . 9 class 𝑚
11		cbl 20497	. . . . . . . . 9 class ball
12	10, 11	cfv 6418	. . . . . . . 8 class (ball‘𝑚)
13	6, 8, 12	co 7255	. . . . . . 7 class (𝑦(ball‘𝑚)𝑟)
14	4, 13	wceq 1539	. . . . . 6 wff 𝑥 = (𝑦(ball‘𝑚)𝑟)
15		crp 12659	. . . . . 6 class ℝ+
16	14, 7, 15	wrex 3064	. . . . 5 wff ∃𝑟 ∈ ℝ+ 𝑥 = (𝑦(ball‘𝑚)𝑟)
17	16, 5, 4	wral 3063	. . . 4 wff ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑥 = (𝑦(ball‘𝑚)𝑟)
18		cmet 20496	. . . . 5 class Met
19	4, 18	cfv 6418	. . . 4 class (Met‘𝑥)
20	17, 9, 19	crab 3067	. . 3 class {𝑚 ∈ (Met‘𝑥) ∣ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑥 = (𝑦(ball‘𝑚)𝑟)}
21	2, 3, 20	cmpt 5153	. 2 class (𝑥 ∈ V ↦ {𝑚 ∈ (Met‘𝑥) ∣ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑥 = (𝑦(ball‘𝑚)𝑟)})
22	1, 21	wceq 1539	1 wff Bnd = (𝑥 ∈ V ↦ {𝑚 ∈ (Met‘𝑥) ∣ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑥 = (𝑦(ball‘𝑚)𝑟)})

This definition is referenced by:  isbnd  35865