# Metamath Proof Explorer

## Theorem sstotbnd3

Description: Use a net that is not necessarily finite, but for which only finitely many balls meet the subset. (Contributed by Mario Carneiro, 14-Sep-2015)

Ref Expression
Hypothesis sstotbnd.2 𝑁 = ( 𝑀 ↾ ( 𝑌 × 𝑌 ) )
Assertion sstotbnd3 ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌𝑋 ) → ( 𝑁 ∈ ( TotBnd ‘ 𝑌 ) ↔ ∀ 𝑑 ∈ ℝ+𝑣 ∈ 𝒫 𝑋 ( 𝑌 𝑥𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∧ { 𝑥𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ≠ ∅ } ∈ Fin ) ) )

### Proof

Step Hyp Ref Expression
1 sstotbnd.2 𝑁 = ( 𝑀 ↾ ( 𝑌 × 𝑌 ) )
2 1 sstotbnd2 ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌𝑋 ) → ( 𝑁 ∈ ( TotBnd ‘ 𝑌 ) ↔ ∀ 𝑑 ∈ ℝ+𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑌 𝑥𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) )
3 elin ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ↔ ( 𝑣 ∈ 𝒫 𝑋𝑣 ∈ Fin ) )
4 rabfi ( 𝑣 ∈ Fin → { 𝑥𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ≠ ∅ } ∈ Fin )
5 4 anim2i ( ( 𝑣 ∈ 𝒫 𝑋𝑣 ∈ Fin ) → ( 𝑣 ∈ 𝒫 𝑋 ∧ { 𝑥𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ≠ ∅ } ∈ Fin ) )
6 3 5 sylbi ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) → ( 𝑣 ∈ 𝒫 𝑋 ∧ { 𝑥𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ≠ ∅ } ∈ Fin ) )
7 6 anim2i ( ( 𝑌 𝑥𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∧ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( 𝑌 𝑥𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∧ ( 𝑣 ∈ 𝒫 𝑋 ∧ { 𝑥𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ≠ ∅ } ∈ Fin ) ) )
8 7 ancoms ( ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 𝑥𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) → ( 𝑌 𝑥𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∧ ( 𝑣 ∈ 𝒫 𝑋 ∧ { 𝑥𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ≠ ∅ } ∈ Fin ) ) )
9 an12 ( ( 𝑌 𝑥𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∧ ( 𝑣 ∈ 𝒫 𝑋 ∧ { 𝑥𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ≠ ∅ } ∈ Fin ) ) ↔ ( 𝑣 ∈ 𝒫 𝑋 ∧ ( 𝑌 𝑥𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∧ { 𝑥𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ≠ ∅ } ∈ Fin ) ) )
10 8 9 sylib ( ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 𝑥𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) → ( 𝑣 ∈ 𝒫 𝑋 ∧ ( 𝑌 𝑥𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∧ { 𝑥𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ≠ ∅ } ∈ Fin ) ) )
11 10 reximi2 ( ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑌 𝑥𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) → ∃ 𝑣 ∈ 𝒫 𝑋 ( 𝑌 𝑥𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∧ { 𝑥𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ≠ ∅ } ∈ Fin ) )
12 11 ralimi ( ∀ 𝑑 ∈ ℝ+𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑌 𝑥𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) → ∀ 𝑑 ∈ ℝ+𝑣 ∈ 𝒫 𝑋 ( 𝑌 𝑥𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∧ { 𝑥𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ≠ ∅ } ∈ Fin ) )
13 2 12 syl6bi ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌𝑋 ) → ( 𝑁 ∈ ( TotBnd ‘ 𝑌 ) → ∀ 𝑑 ∈ ℝ+𝑣 ∈ 𝒫 𝑋 ( 𝑌 𝑥𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∧ { 𝑥𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ≠ ∅ } ∈ Fin ) ) )
14 ssrab2 { 𝑥𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ≠ ∅ } ⊆ 𝑣
15 elpwi ( 𝑣 ∈ 𝒫 𝑋𝑣𝑋 )
16 15 ad2antlr ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌𝑋 ) ∧ 𝑣 ∈ 𝒫 𝑋 ) ∧ ( 𝑌 𝑥𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∧ { 𝑥𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ≠ ∅ } ∈ Fin ) ) → 𝑣𝑋 )
17 14 16 sstrid ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌𝑋 ) ∧ 𝑣 ∈ 𝒫 𝑋 ) ∧ ( 𝑌 𝑥𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∧ { 𝑥𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ≠ ∅ } ∈ Fin ) ) → { 𝑥𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ≠ ∅ } ⊆ 𝑋 )
18 simprr ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌𝑋 ) ∧ 𝑣 ∈ 𝒫 𝑋 ) ∧ ( 𝑌 𝑥𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∧ { 𝑥𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ≠ ∅ } ∈ Fin ) ) → { 𝑥𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ≠ ∅ } ∈ Fin )
19 elfpw ( { 𝑥𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ≠ ∅ } ∈ ( 𝒫 𝑋 ∩ Fin ) ↔ ( { 𝑥𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ≠ ∅ } ⊆ 𝑋 ∧ { 𝑥𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ≠ ∅ } ∈ Fin ) )
20 17 18 19 sylanbrc ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌𝑋 ) ∧ 𝑣 ∈ 𝒫 𝑋 ) ∧ ( 𝑌 𝑥𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∧ { 𝑥𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ≠ ∅ } ∈ Fin ) ) → { 𝑥𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ≠ ∅ } ∈ ( 𝒫 𝑋 ∩ Fin ) )
21 ssel2 ( ( 𝑌 𝑥𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∧ 𝑧𝑌 ) → 𝑧 𝑥𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) )
22 eliun ( 𝑧 𝑥𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ↔ ∃ 𝑥𝑣 𝑧 ∈ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) )
23 21 22 sylib ( ( 𝑌 𝑥𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∧ 𝑧𝑌 ) → ∃ 𝑥𝑣 𝑧 ∈ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) )
24 inelcm ( ( 𝑧 ∈ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∧ 𝑧𝑌 ) → ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ≠ ∅ )
25 24 expcom ( 𝑧𝑌 → ( 𝑧 ∈ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) → ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ≠ ∅ ) )
26 25 ancrd ( 𝑧𝑌 → ( 𝑧 ∈ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) → ( ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ≠ ∅ ∧ 𝑧 ∈ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ) )
27 26 reximdv ( 𝑧𝑌 → ( ∃ 𝑥𝑣 𝑧 ∈ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) → ∃ 𝑥𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ≠ ∅ ∧ 𝑧 ∈ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ) )
28 27 impcom ( ( ∃ 𝑥𝑣 𝑧 ∈ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∧ 𝑧𝑌 ) → ∃ 𝑥𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ≠ ∅ ∧ 𝑧 ∈ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) )
29 23 28 sylancom ( ( 𝑌 𝑥𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∧ 𝑧𝑌 ) → ∃ 𝑥𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ≠ ∅ ∧ 𝑧 ∈ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) )
30 eliun ( 𝑧 𝑦 ∈ { 𝑥𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ≠ ∅ } ( 𝑦 ( ball ‘ 𝑀 ) 𝑑 ) ↔ ∃ 𝑦 ∈ { 𝑥𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ≠ ∅ } 𝑧 ∈ ( 𝑦 ( ball ‘ 𝑀 ) 𝑑 ) )
31 oveq1 ( 𝑦 = 𝑥 → ( 𝑦 ( ball ‘ 𝑀 ) 𝑑 ) = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) )
32 31 eleq2d ( 𝑦 = 𝑥 → ( 𝑧 ∈ ( 𝑦 ( ball ‘ 𝑀 ) 𝑑 ) ↔ 𝑧 ∈ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) )
33 32 rexrab2 ( ∃ 𝑦 ∈ { 𝑥𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ≠ ∅ } 𝑧 ∈ ( 𝑦 ( ball ‘ 𝑀 ) 𝑑 ) ↔ ∃ 𝑥𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ≠ ∅ ∧ 𝑧 ∈ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) )
34 30 33 bitri ( 𝑧 𝑦 ∈ { 𝑥𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ≠ ∅ } ( 𝑦 ( ball ‘ 𝑀 ) 𝑑 ) ↔ ∃ 𝑥𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ≠ ∅ ∧ 𝑧 ∈ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) )
35 29 34 sylibr ( ( 𝑌 𝑥𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∧ 𝑧𝑌 ) → 𝑧 𝑦 ∈ { 𝑥𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ≠ ∅ } ( 𝑦 ( ball ‘ 𝑀 ) 𝑑 ) )
36 35 ex ( 𝑌 𝑥𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) → ( 𝑧𝑌𝑧 𝑦 ∈ { 𝑥𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ≠ ∅ } ( 𝑦 ( ball ‘ 𝑀 ) 𝑑 ) ) )
37 36 ssrdv ( 𝑌 𝑥𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) → 𝑌 𝑦 ∈ { 𝑥𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ≠ ∅ } ( 𝑦 ( ball ‘ 𝑀 ) 𝑑 ) )
38 37 ad2antrl ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌𝑋 ) ∧ 𝑣 ∈ 𝒫 𝑋 ) ∧ ( 𝑌 𝑥𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∧ { 𝑥𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ≠ ∅ } ∈ Fin ) ) → 𝑌 𝑦 ∈ { 𝑥𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ≠ ∅ } ( 𝑦 ( ball ‘ 𝑀 ) 𝑑 ) )
39 iuneq1 ( 𝑤 = { 𝑥𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ≠ ∅ } → 𝑦𝑤 ( 𝑦 ( ball ‘ 𝑀 ) 𝑑 ) = 𝑦 ∈ { 𝑥𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ≠ ∅ } ( 𝑦 ( ball ‘ 𝑀 ) 𝑑 ) )
40 39 sseq2d ( 𝑤 = { 𝑥𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ≠ ∅ } → ( 𝑌 𝑦𝑤 ( 𝑦 ( ball ‘ 𝑀 ) 𝑑 ) ↔ 𝑌 𝑦 ∈ { 𝑥𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ≠ ∅ } ( 𝑦 ( ball ‘ 𝑀 ) 𝑑 ) ) )
41 40 rspcev ( ( { 𝑥𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ≠ ∅ } ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 𝑦 ∈ { 𝑥𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ≠ ∅ } ( 𝑦 ( ball ‘ 𝑀 ) 𝑑 ) ) → ∃ 𝑤 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑌 𝑦𝑤 ( 𝑦 ( ball ‘ 𝑀 ) 𝑑 ) )
42 20 38 41 syl2anc ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌𝑋 ) ∧ 𝑣 ∈ 𝒫 𝑋 ) ∧ ( 𝑌 𝑥𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∧ { 𝑥𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ≠ ∅ } ∈ Fin ) ) → ∃ 𝑤 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑌 𝑦𝑤 ( 𝑦 ( ball ‘ 𝑀 ) 𝑑 ) )
43 42 rexlimdva2 ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌𝑋 ) → ( ∃ 𝑣 ∈ 𝒫 𝑋 ( 𝑌 𝑥𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∧ { 𝑥𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ≠ ∅ } ∈ Fin ) → ∃ 𝑤 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑌 𝑦𝑤 ( 𝑦 ( ball ‘ 𝑀 ) 𝑑 ) ) )
44 43 ralimdv ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌𝑋 ) → ( ∀ 𝑑 ∈ ℝ+𝑣 ∈ 𝒫 𝑋 ( 𝑌 𝑥𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∧ { 𝑥𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ≠ ∅ } ∈ Fin ) → ∀ 𝑑 ∈ ℝ+𝑤 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑌 𝑦𝑤 ( 𝑦 ( ball ‘ 𝑀 ) 𝑑 ) ) )
45 1 sstotbnd2 ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌𝑋 ) → ( 𝑁 ∈ ( TotBnd ‘ 𝑌 ) ↔ ∀ 𝑑 ∈ ℝ+𝑤 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑌 𝑦𝑤 ( 𝑦 ( ball ‘ 𝑀 ) 𝑑 ) ) )
46 44 45 sylibrd ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌𝑋 ) → ( ∀ 𝑑 ∈ ℝ+𝑣 ∈ 𝒫 𝑋 ( 𝑌 𝑥𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∧ { 𝑥𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ≠ ∅ } ∈ Fin ) → 𝑁 ∈ ( TotBnd ‘ 𝑌 ) ) )
47 13 46 impbid ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌𝑋 ) → ( 𝑁 ∈ ( TotBnd ‘ 𝑌 ) ↔ ∀ 𝑑 ∈ ℝ+𝑣 ∈ 𝒫 𝑋 ( 𝑌 𝑥𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∧ { 𝑥𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ≠ ∅ } ∈ Fin ) ) )