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 34915
 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 34913 . 2 class TotBnd
2 vx . . 3 setvar 𝑥
3 cvv 3499 . . 3 class V
4 vv . . . . . . . . . 10 setvar 𝑣
54cv 1529 . . . . . . . . 9 class 𝑣
65cuni 4836 . . . . . . . 8 class 𝑣
72cv 1529 . . . . . . . 8 class 𝑥
86, 7wceq 1530 . . . . . . 7 wff 𝑣 = 𝑥
9 vb . . . . . . . . . . 11 setvar 𝑏
109cv 1529 . . . . . . . . . 10 class 𝑏
11 vy . . . . . . . . . . . 12 setvar 𝑦
1211cv 1529 . . . . . . . . . . 11 class 𝑦
13 vd . . . . . . . . . . . 12 setvar 𝑑
1413cv 1529 . . . . . . . . . . 11 class 𝑑
15 vm . . . . . . . . . . . . 13 setvar 𝑚
1615cv 1529 . . . . . . . . . . . 12 class 𝑚
17 cbl 20448 . . . . . . . . . . . 12 class ball
1816, 17cfv 6351 . . . . . . . . . . 11 class (ball‘𝑚)
1912, 14, 18co 7151 . . . . . . . . . 10 class (𝑦(ball‘𝑚)𝑑)
2010, 19wceq 1530 . . . . . . . . 9 wff 𝑏 = (𝑦(ball‘𝑚)𝑑)
2120, 11, 7wrex 3143 . . . . . . . 8 wff 𝑦𝑥 𝑏 = (𝑦(ball‘𝑚)𝑑)
2221, 9, 5wral 3142 . . . . . . 7 wff 𝑏𝑣𝑦𝑥 𝑏 = (𝑦(ball‘𝑚)𝑑)
238, 22wa 396 . . . . . 6 wff ( 𝑣 = 𝑥 ∧ ∀𝑏𝑣𝑦𝑥 𝑏 = (𝑦(ball‘𝑚)𝑑))
24 cfn 8501 . . . . . 6 class Fin
2523, 4, 24wrex 3143 . . . . 5 wff 𝑣 ∈ Fin ( 𝑣 = 𝑥 ∧ ∀𝑏𝑣𝑦𝑥 𝑏 = (𝑦(ball‘𝑚)𝑑))
26 crp 12382 . . . . 5 class +
2725, 13, 26wral 3142 . . . 4 wff 𝑑 ∈ ℝ+𝑣 ∈ Fin ( 𝑣 = 𝑥 ∧ ∀𝑏𝑣𝑦𝑥 𝑏 = (𝑦(ball‘𝑚)𝑑))
28 cmet 20447 . . . . 5 class Met
297, 28cfv 6351 . . . 4 class (Met‘𝑥)
3027, 15, 29crab 3146 . . 3 class {𝑚 ∈ (Met‘𝑥) ∣ ∀𝑑 ∈ ℝ+𝑣 ∈ Fin ( 𝑣 = 𝑥 ∧ ∀𝑏𝑣𝑦𝑥 𝑏 = (𝑦(ball‘𝑚)𝑑))}
312, 3, 30cmpt 5142 . 2 class (𝑥 ∈ V ↦ {𝑚 ∈ (Met‘𝑥) ∣ ∀𝑑 ∈ ℝ+𝑣 ∈ Fin ( 𝑣 = 𝑥 ∧ ∀𝑏𝑣𝑦𝑥 𝑏 = (𝑦(ball‘𝑚)𝑑))})
321, 31wceq 1530 1 wff TotBnd = (𝑥 ∈ V ↦ {𝑚 ∈ (Met‘𝑥) ∣ ∀𝑑 ∈ ℝ+𝑣 ∈ Fin ( 𝑣 = 𝑥 ∧ ∀𝑏𝑣𝑦𝑥 𝑏 = (𝑦(ball‘𝑚)𝑑))})
 Colors of variables: wff setvar class This definition is referenced by:  istotbnd  34916
 Copyright terms: Public domain W3C validator