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 36722
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 36720 . 2 class TotBnd
2 vx . . 3 setvar π‘₯
3 cvv 3474 . . 3 class V
4 vv . . . . . . . . . 10 setvar 𝑣
54cv 1540 . . . . . . . . 9 class 𝑣
65cuni 4908 . . . . . . . 8 class βˆͺ 𝑣
72cv 1540 . . . . . . . 8 class π‘₯
86, 7wceq 1541 . . . . . . 7 wff βˆͺ 𝑣 = π‘₯
9 vb . . . . . . . . . . 11 setvar 𝑏
109cv 1540 . . . . . . . . . 10 class 𝑏
11 vy . . . . . . . . . . . 12 setvar 𝑦
1211cv 1540 . . . . . . . . . . 11 class 𝑦
13 vd . . . . . . . . . . . 12 setvar 𝑑
1413cv 1540 . . . . . . . . . . 11 class 𝑑
15 vm . . . . . . . . . . . . 13 setvar π‘š
1615cv 1540 . . . . . . . . . . . 12 class π‘š
17 cbl 20937 . . . . . . . . . . . 12 class ball
1816, 17cfv 6543 . . . . . . . . . . 11 class (ballβ€˜π‘š)
1912, 14, 18co 7411 . . . . . . . . . 10 class (𝑦(ballβ€˜π‘š)𝑑)
2010, 19wceq 1541 . . . . . . . . 9 wff 𝑏 = (𝑦(ballβ€˜π‘š)𝑑)
2120, 11, 7wrex 3070 . . . . . . . 8 wff βˆƒπ‘¦ ∈ π‘₯ 𝑏 = (𝑦(ballβ€˜π‘š)𝑑)
2221, 9, 5wral 3061 . . . . . . 7 wff βˆ€π‘ ∈ 𝑣 βˆƒπ‘¦ ∈ π‘₯ 𝑏 = (𝑦(ballβ€˜π‘š)𝑑)
238, 22wa 396 . . . . . 6 wff (βˆͺ 𝑣 = π‘₯ ∧ βˆ€π‘ ∈ 𝑣 βˆƒπ‘¦ ∈ π‘₯ 𝑏 = (𝑦(ballβ€˜π‘š)𝑑))
24 cfn 8941 . . . . . 6 class Fin
2523, 4, 24wrex 3070 . . . . 5 wff βˆƒπ‘£ ∈ Fin (βˆͺ 𝑣 = π‘₯ ∧ βˆ€π‘ ∈ 𝑣 βˆƒπ‘¦ ∈ π‘₯ 𝑏 = (𝑦(ballβ€˜π‘š)𝑑))
26 crp 12976 . . . . 5 class ℝ+
2725, 13, 26wral 3061 . . . 4 wff βˆ€π‘‘ ∈ ℝ+ βˆƒπ‘£ ∈ Fin (βˆͺ 𝑣 = π‘₯ ∧ βˆ€π‘ ∈ 𝑣 βˆƒπ‘¦ ∈ π‘₯ 𝑏 = (𝑦(ballβ€˜π‘š)𝑑))
28 cmet 20936 . . . . 5 class Met
297, 28cfv 6543 . . . 4 class (Metβ€˜π‘₯)
3027, 15, 29crab 3432 . . 3 class {π‘š ∈ (Metβ€˜π‘₯) ∣ βˆ€π‘‘ ∈ ℝ+ βˆƒπ‘£ ∈ Fin (βˆͺ 𝑣 = π‘₯ ∧ βˆ€π‘ ∈ 𝑣 βˆƒπ‘¦ ∈ π‘₯ 𝑏 = (𝑦(ballβ€˜π‘š)𝑑))}
312, 3, 30cmpt 5231 . 2 class (π‘₯ ∈ V ↦ {π‘š ∈ (Metβ€˜π‘₯) ∣ βˆ€π‘‘ ∈ ℝ+ βˆƒπ‘£ ∈ Fin (βˆͺ 𝑣 = π‘₯ ∧ βˆ€π‘ ∈ 𝑣 βˆƒπ‘¦ ∈ π‘₯ 𝑏 = (𝑦(ballβ€˜π‘š)𝑑))})
321, 31wceq 1541 1 wff TotBnd = (π‘₯ ∈ V ↦ {π‘š ∈ (Metβ€˜π‘₯) ∣ βˆ€π‘‘ ∈ ℝ+ βˆƒπ‘£ ∈ Fin (βˆͺ 𝑣 = π‘₯ ∧ βˆ€π‘ ∈ 𝑣 βˆƒπ‘¦ ∈ π‘₯ 𝑏 = (𝑦(ballβ€˜π‘š)𝑑))})
Colors of variables: wff setvar class
This definition is referenced by:  istotbnd  36723
  Copyright terms: Public domain W3C validator