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

Definition df-totbnd 33899
Description: Define the class of totally bounded metrics. A metric space is totally bounded iff it can be covered by a finite number of balls of any given radius. (Contributed by Jeff Madsen, 2-Sep-2009.)
Assertion
Ref Expression
df-totbnd TotBnd = (𝑥 ∈ V ↦ {𝑚 ∈ (Met‘𝑥) ∣ ∀𝑑 ∈ ℝ+𝑣 ∈ Fin ( 𝑣 = 𝑥 ∧ ∀𝑏𝑣𝑦𝑥 𝑏 = (𝑦(ball‘𝑚)𝑑))})
Distinct variable group:   𝑏,𝑑,𝑚,𝑣,𝑥,𝑦

Detailed syntax breakdown of Definition df-totbnd
StepHypRef Expression
1 ctotbnd 33897 . 2 class TotBnd
2 vx . . 3 setvar 𝑥
3 cvv 3351 . . 3 class V
4 vv . . . . . . . . . 10 setvar 𝑣
54cv 1630 . . . . . . . . 9 class 𝑣
65cuni 4574 . . . . . . . 8 class 𝑣
72cv 1630 . . . . . . . 8 class 𝑥
86, 7wceq 1631 . . . . . . 7 wff 𝑣 = 𝑥
9 vb . . . . . . . . . . 11 setvar 𝑏
109cv 1630 . . . . . . . . . 10 class 𝑏
11 vy . . . . . . . . . . . 12 setvar 𝑦
1211cv 1630 . . . . . . . . . . 11 class 𝑦
13 vd . . . . . . . . . . . 12 setvar 𝑑
1413cv 1630 . . . . . . . . . . 11 class 𝑑
15 vm . . . . . . . . . . . . 13 setvar 𝑚
1615cv 1630 . . . . . . . . . . . 12 class 𝑚
17 cbl 19948 . . . . . . . . . . . 12 class ball
1816, 17cfv 6031 . . . . . . . . . . 11 class (ball‘𝑚)
1912, 14, 18co 6793 . . . . . . . . . 10 class (𝑦(ball‘𝑚)𝑑)
2010, 19wceq 1631 . . . . . . . . 9 wff 𝑏 = (𝑦(ball‘𝑚)𝑑)
2120, 11, 7wrex 3062 . . . . . . . 8 wff 𝑦𝑥 𝑏 = (𝑦(ball‘𝑚)𝑑)
2221, 9, 5wral 3061 . . . . . . 7 wff 𝑏𝑣𝑦𝑥 𝑏 = (𝑦(ball‘𝑚)𝑑)
238, 22wa 382 . . . . . 6 wff ( 𝑣 = 𝑥 ∧ ∀𝑏𝑣𝑦𝑥 𝑏 = (𝑦(ball‘𝑚)𝑑))
24 cfn 8109 . . . . . 6 class Fin
2523, 4, 24wrex 3062 . . . . 5 wff 𝑣 ∈ Fin ( 𝑣 = 𝑥 ∧ ∀𝑏𝑣𝑦𝑥 𝑏 = (𝑦(ball‘𝑚)𝑑))
26 crp 12035 . . . . 5 class +
2725, 13, 26wral 3061 . . . 4 wff 𝑑 ∈ ℝ+𝑣 ∈ Fin ( 𝑣 = 𝑥 ∧ ∀𝑏𝑣𝑦𝑥 𝑏 = (𝑦(ball‘𝑚)𝑑))
28 cme 19947 . . . . 5 class Met
297, 28cfv 6031 . . . 4 class (Met‘𝑥)
3027, 15, 29crab 3065 . . 3 class {𝑚 ∈ (Met‘𝑥) ∣ ∀𝑑 ∈ ℝ+𝑣 ∈ Fin ( 𝑣 = 𝑥 ∧ ∀𝑏𝑣𝑦𝑥 𝑏 = (𝑦(ball‘𝑚)𝑑))}
312, 3, 30cmpt 4863 . 2 class (𝑥 ∈ V ↦ {𝑚 ∈ (Met‘𝑥) ∣ ∀𝑑 ∈ ℝ+𝑣 ∈ Fin ( 𝑣 = 𝑥 ∧ ∀𝑏𝑣𝑦𝑥 𝑏 = (𝑦(ball‘𝑚)𝑑))})
321, 31wceq 1631 1 wff TotBnd = (𝑥 ∈ V ↦ {𝑚 ∈ (Met‘𝑥) ∣ ∀𝑑 ∈ ℝ+𝑣 ∈ Fin ( 𝑣 = 𝑥 ∧ ∀𝑏𝑣𝑦𝑥 𝑏 = (𝑦(ball‘𝑚)𝑑))})
Colors of variables: wff setvar class
This definition is referenced by:  istotbnd  33900
  Copyright terms: Public domain W3C validator