This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimtrdi ⊢ ( ( 𝑀 ∈ ( 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 ) ) )