Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-bnd Structured version   Visualization version   GIF version

Definition df-bnd 33910
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
StepHypRef Expression
1 cbnd 33898 . 2 class Bnd
2 vx . . 3 setvar 𝑥
3 cvv 3351 . . 3 class V
42cv 1630 . . . . . . 7 class 𝑥
5 vy . . . . . . . . 9 setvar 𝑦
65cv 1630 . . . . . . . 8 class 𝑦
7 vr . . . . . . . . 9 setvar 𝑟
87cv 1630 . . . . . . . 8 class 𝑟
9 vm . . . . . . . . . 10 setvar 𝑚
109cv 1630 . . . . . . . . 9 class 𝑚
11 cbl 19948 . . . . . . . . 9 class ball
1210, 11cfv 6031 . . . . . . . 8 class (ball‘𝑚)
136, 8, 12co 6793 . . . . . . 7 class (𝑦(ball‘𝑚)𝑟)
144, 13wceq 1631 . . . . . 6 wff 𝑥 = (𝑦(ball‘𝑚)𝑟)
15 crp 12035 . . . . . 6 class +
1614, 7, 15wrex 3062 . . . . 5 wff 𝑟 ∈ ℝ+ 𝑥 = (𝑦(ball‘𝑚)𝑟)
1716, 5, 4wral 3061 . . . 4 wff 𝑦𝑥𝑟 ∈ ℝ+ 𝑥 = (𝑦(ball‘𝑚)𝑟)
18 cme 19947 . . . . 5 class Met
194, 18cfv 6031 . . . 4 class (Met‘𝑥)
2017, 9, 19crab 3065 . . 3 class {𝑚 ∈ (Met‘𝑥) ∣ ∀𝑦𝑥𝑟 ∈ ℝ+ 𝑥 = (𝑦(ball‘𝑚)𝑟)}
212, 3, 20cmpt 4863 . 2 class (𝑥 ∈ V ↦ {𝑚 ∈ (Met‘𝑥) ∣ ∀𝑦𝑥𝑟 ∈ ℝ+ 𝑥 = (𝑦(ball‘𝑚)𝑟)})
221, 21wceq 1631 1 wff Bnd = (𝑥 ∈ V ↦ {𝑚 ∈ (Met‘𝑥) ∣ ∀𝑦𝑥𝑟 ∈ ℝ+ 𝑥 = (𝑦(ball‘𝑚)𝑟)})
Colors of variables: wff setvar class
This definition is referenced by:  isbnd  33911
  Copyright terms: Public domain W3C validator