Metamath Proof Explorer


Theorem ssbnd

Description: A subset of a metric space is bounded iff it is contained in a ball around P , for any P in the larger space. (Contributed by Mario Carneiro, 14-Sep-2015)

Ref Expression
Hypothesis ssbnd.2 𝑁 = ( 𝑀 ↾ ( 𝑌 × 𝑌 ) )
Assertion ssbnd ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃𝑋 ) → ( 𝑁 ∈ ( Bnd ‘ 𝑌 ) ↔ ∃ 𝑑 ∈ ℝ 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) )

Proof

Step Hyp Ref Expression
1 ssbnd.2 𝑁 = ( 𝑀 ↾ ( 𝑌 × 𝑌 ) )
2 0re 0 ∈ ℝ
3 2 ne0ii ℝ ≠ ∅
4 0ss ∅ ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 )
5 sseq1 ( 𝑌 = ∅ → ( 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ↔ ∅ ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) )
6 4 5 mpbiri ( 𝑌 = ∅ → 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) )
7 6 ralrimivw ( 𝑌 = ∅ → ∀ 𝑑 ∈ ℝ 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) )
8 r19.2z ( ( ℝ ≠ ∅ ∧ ∀ 𝑑 ∈ ℝ 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) → ∃ 𝑑 ∈ ℝ 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) )
9 3 7 8 sylancr ( 𝑌 = ∅ → ∃ 𝑑 ∈ ℝ 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) )
10 9 a1i ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃𝑋 ) ∧ 𝑁 ∈ ( Bnd ‘ 𝑌 ) ) → ( 𝑌 = ∅ → ∃ 𝑑 ∈ ℝ 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) )
11 isbnd2 ( ( 𝑁 ∈ ( Bnd ‘ 𝑌 ) ∧ 𝑌 ≠ ∅ ) ↔ ( 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ ∃ 𝑦𝑌𝑟 ∈ ℝ+ 𝑌 = ( 𝑦 ( ball ‘ 𝑁 ) 𝑟 ) ) )
12 simplll ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦𝑌𝑟 ∈ ℝ+ ) ) → 𝑀 ∈ ( Met ‘ 𝑋 ) )
13 1 dmeqi dom 𝑁 = dom ( 𝑀 ↾ ( 𝑌 × 𝑌 ) )
14 dmres dom ( 𝑀 ↾ ( 𝑌 × 𝑌 ) ) = ( ( 𝑌 × 𝑌 ) ∩ dom 𝑀 )
15 13 14 eqtri dom 𝑁 = ( ( 𝑌 × 𝑌 ) ∩ dom 𝑀 )
16 xmetf ( 𝑁 ∈ ( ∞Met ‘ 𝑌 ) → 𝑁 : ( 𝑌 × 𝑌 ) ⟶ ℝ* )
17 16 fdmd ( 𝑁 ∈ ( ∞Met ‘ 𝑌 ) → dom 𝑁 = ( 𝑌 × 𝑌 ) )
18 15 17 eqtr3id ( 𝑁 ∈ ( ∞Met ‘ 𝑌 ) → ( ( 𝑌 × 𝑌 ) ∩ dom 𝑀 ) = ( 𝑌 × 𝑌 ) )
19 df-ss ( ( 𝑌 × 𝑌 ) ⊆ dom 𝑀 ↔ ( ( 𝑌 × 𝑌 ) ∩ dom 𝑀 ) = ( 𝑌 × 𝑌 ) )
20 18 19 sylibr ( 𝑁 ∈ ( ∞Met ‘ 𝑌 ) → ( 𝑌 × 𝑌 ) ⊆ dom 𝑀 )
21 20 ad2antlr ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦𝑌𝑟 ∈ ℝ+ ) ) → ( 𝑌 × 𝑌 ) ⊆ dom 𝑀 )
22 metf ( 𝑀 ∈ ( Met ‘ 𝑋 ) → 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ℝ )
23 22 fdmd ( 𝑀 ∈ ( Met ‘ 𝑋 ) → dom 𝑀 = ( 𝑋 × 𝑋 ) )
24 23 ad3antrrr ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦𝑌𝑟 ∈ ℝ+ ) ) → dom 𝑀 = ( 𝑋 × 𝑋 ) )
25 21 24 sseqtrd ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦𝑌𝑟 ∈ ℝ+ ) ) → ( 𝑌 × 𝑌 ) ⊆ ( 𝑋 × 𝑋 ) )
26 dmss ( ( 𝑌 × 𝑌 ) ⊆ ( 𝑋 × 𝑋 ) → dom ( 𝑌 × 𝑌 ) ⊆ dom ( 𝑋 × 𝑋 ) )
27 25 26 syl ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦𝑌𝑟 ∈ ℝ+ ) ) → dom ( 𝑌 × 𝑌 ) ⊆ dom ( 𝑋 × 𝑋 ) )
28 dmxpid dom ( 𝑌 × 𝑌 ) = 𝑌
29 dmxpid dom ( 𝑋 × 𝑋 ) = 𝑋
30 27 28 29 3sstr3g ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦𝑌𝑟 ∈ ℝ+ ) ) → 𝑌𝑋 )
31 simprl ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦𝑌𝑟 ∈ ℝ+ ) ) → 𝑦𝑌 )
32 30 31 sseldd ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦𝑌𝑟 ∈ ℝ+ ) ) → 𝑦𝑋 )
33 simpllr ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦𝑌𝑟 ∈ ℝ+ ) ) → 𝑃𝑋 )
34 metcl ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑦𝑋𝑃𝑋 ) → ( 𝑦 𝑀 𝑃 ) ∈ ℝ )
35 12 32 33 34 syl3anc ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦𝑌𝑟 ∈ ℝ+ ) ) → ( 𝑦 𝑀 𝑃 ) ∈ ℝ )
36 rpre ( 𝑟 ∈ ℝ+𝑟 ∈ ℝ )
37 36 ad2antll ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦𝑌𝑟 ∈ ℝ+ ) ) → 𝑟 ∈ ℝ )
38 35 37 readdcld ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦𝑌𝑟 ∈ ℝ+ ) ) → ( ( 𝑦 𝑀 𝑃 ) + 𝑟 ) ∈ ℝ )
39 metxmet ( 𝑀 ∈ ( Met ‘ 𝑋 ) → 𝑀 ∈ ( ∞Met ‘ 𝑋 ) )
40 12 39 syl ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦𝑌𝑟 ∈ ℝ+ ) ) → 𝑀 ∈ ( ∞Met ‘ 𝑋 ) )
41 32 31 elind ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦𝑌𝑟 ∈ ℝ+ ) ) → 𝑦 ∈ ( 𝑋𝑌 ) )
42 rpxr ( 𝑟 ∈ ℝ+𝑟 ∈ ℝ* )
43 42 ad2antll ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦𝑌𝑟 ∈ ℝ+ ) ) → 𝑟 ∈ ℝ* )
44 1 blres ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ ( 𝑋𝑌 ) ∧ 𝑟 ∈ ℝ* ) → ( 𝑦 ( ball ‘ 𝑁 ) 𝑟 ) = ( ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ∩ 𝑌 ) )
45 40 41 43 44 syl3anc ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦𝑌𝑟 ∈ ℝ+ ) ) → ( 𝑦 ( ball ‘ 𝑁 ) 𝑟 ) = ( ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ∩ 𝑌 ) )
46 inss1 ( ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ∩ 𝑌 ) ⊆ ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 )
47 35 leidd ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦𝑌𝑟 ∈ ℝ+ ) ) → ( 𝑦 𝑀 𝑃 ) ≤ ( 𝑦 𝑀 𝑃 ) )
48 35 recnd ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦𝑌𝑟 ∈ ℝ+ ) ) → ( 𝑦 𝑀 𝑃 ) ∈ ℂ )
49 37 recnd ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦𝑌𝑟 ∈ ℝ+ ) ) → 𝑟 ∈ ℂ )
50 48 49 pncand ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦𝑌𝑟 ∈ ℝ+ ) ) → ( ( ( 𝑦 𝑀 𝑃 ) + 𝑟 ) − 𝑟 ) = ( 𝑦 𝑀 𝑃 ) )
51 47 50 breqtrrd ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦𝑌𝑟 ∈ ℝ+ ) ) → ( 𝑦 𝑀 𝑃 ) ≤ ( ( ( 𝑦 𝑀 𝑃 ) + 𝑟 ) − 𝑟 ) )
52 blss2 ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦𝑋𝑃𝑋 ) ∧ ( 𝑟 ∈ ℝ ∧ ( ( 𝑦 𝑀 𝑃 ) + 𝑟 ) ∈ ℝ ∧ ( 𝑦 𝑀 𝑃 ) ≤ ( ( ( 𝑦 𝑀 𝑃 ) + 𝑟 ) − 𝑟 ) ) ) → ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ⊆ ( 𝑃 ( ball ‘ 𝑀 ) ( ( 𝑦 𝑀 𝑃 ) + 𝑟 ) ) )
53 40 32 33 37 38 51 52 syl33anc ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦𝑌𝑟 ∈ ℝ+ ) ) → ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ⊆ ( 𝑃 ( ball ‘ 𝑀 ) ( ( 𝑦 𝑀 𝑃 ) + 𝑟 ) ) )
54 46 53 sstrid ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦𝑌𝑟 ∈ ℝ+ ) ) → ( ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ∩ 𝑌 ) ⊆ ( 𝑃 ( ball ‘ 𝑀 ) ( ( 𝑦 𝑀 𝑃 ) + 𝑟 ) ) )
55 45 54 eqsstrd ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦𝑌𝑟 ∈ ℝ+ ) ) → ( 𝑦 ( ball ‘ 𝑁 ) 𝑟 ) ⊆ ( 𝑃 ( ball ‘ 𝑀 ) ( ( 𝑦 𝑀 𝑃 ) + 𝑟 ) ) )
56 oveq2 ( 𝑑 = ( ( 𝑦 𝑀 𝑃 ) + 𝑟 ) → ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) = ( 𝑃 ( ball ‘ 𝑀 ) ( ( 𝑦 𝑀 𝑃 ) + 𝑟 ) ) )
57 56 sseq2d ( 𝑑 = ( ( 𝑦 𝑀 𝑃 ) + 𝑟 ) → ( ( 𝑦 ( ball ‘ 𝑁 ) 𝑟 ) ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ↔ ( 𝑦 ( ball ‘ 𝑁 ) 𝑟 ) ⊆ ( 𝑃 ( ball ‘ 𝑀 ) ( ( 𝑦 𝑀 𝑃 ) + 𝑟 ) ) ) )
58 57 rspcev ( ( ( ( 𝑦 𝑀 𝑃 ) + 𝑟 ) ∈ ℝ ∧ ( 𝑦 ( ball ‘ 𝑁 ) 𝑟 ) ⊆ ( 𝑃 ( ball ‘ 𝑀 ) ( ( 𝑦 𝑀 𝑃 ) + 𝑟 ) ) ) → ∃ 𝑑 ∈ ℝ ( 𝑦 ( ball ‘ 𝑁 ) 𝑟 ) ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) )
59 38 55 58 syl2anc ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦𝑌𝑟 ∈ ℝ+ ) ) → ∃ 𝑑 ∈ ℝ ( 𝑦 ( ball ‘ 𝑁 ) 𝑟 ) ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) )
60 sseq1 ( 𝑌 = ( 𝑦 ( ball ‘ 𝑁 ) 𝑟 ) → ( 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ↔ ( 𝑦 ( ball ‘ 𝑁 ) 𝑟 ) ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) )
61 60 rexbidv ( 𝑌 = ( 𝑦 ( ball ‘ 𝑁 ) 𝑟 ) → ( ∃ 𝑑 ∈ ℝ 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ↔ ∃ 𝑑 ∈ ℝ ( 𝑦 ( ball ‘ 𝑁 ) 𝑟 ) ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) )
62 59 61 syl5ibrcom ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑦𝑌𝑟 ∈ ℝ+ ) ) → ( 𝑌 = ( 𝑦 ( ball ‘ 𝑁 ) 𝑟 ) → ∃ 𝑑 ∈ ℝ 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) )
63 62 rexlimdvva ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) → ( ∃ 𝑦𝑌𝑟 ∈ ℝ+ 𝑌 = ( 𝑦 ( ball ‘ 𝑁 ) 𝑟 ) → ∃ 𝑑 ∈ ℝ 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) )
64 63 expimpd ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃𝑋 ) → ( ( 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ ∃ 𝑦𝑌𝑟 ∈ ℝ+ 𝑌 = ( 𝑦 ( ball ‘ 𝑁 ) 𝑟 ) ) → ∃ 𝑑 ∈ ℝ 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) )
65 11 64 syl5bi ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃𝑋 ) → ( ( 𝑁 ∈ ( Bnd ‘ 𝑌 ) ∧ 𝑌 ≠ ∅ ) → ∃ 𝑑 ∈ ℝ 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) )
66 65 expdimp ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃𝑋 ) ∧ 𝑁 ∈ ( Bnd ‘ 𝑌 ) ) → ( 𝑌 ≠ ∅ → ∃ 𝑑 ∈ ℝ 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) )
67 10 66 pm2.61dne ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃𝑋 ) ∧ 𝑁 ∈ ( Bnd ‘ 𝑌 ) ) → ∃ 𝑑 ∈ ℝ 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) )
68 67 ex ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃𝑋 ) → ( 𝑁 ∈ ( Bnd ‘ 𝑌 ) → ∃ 𝑑 ∈ ℝ 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) )
69 simprr ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃𝑋 ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) ) → 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) )
70 xpss12 ( ( 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ∧ 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) → ( 𝑌 × 𝑌 ) ⊆ ( ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) × ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) )
71 69 69 70 syl2anc ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃𝑋 ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) ) → ( 𝑌 × 𝑌 ) ⊆ ( ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) × ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) )
72 71 resabs1d ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃𝑋 ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) ) → ( ( 𝑀 ↾ ( ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) × ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) ) ↾ ( 𝑌 × 𝑌 ) ) = ( 𝑀 ↾ ( 𝑌 × 𝑌 ) ) )
73 72 1 eqtr4di ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃𝑋 ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) ) → ( ( 𝑀 ↾ ( ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) × ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) ) ↾ ( 𝑌 × 𝑌 ) ) = 𝑁 )
74 blbnd ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑑 ∈ ℝ ) → ( 𝑀 ↾ ( ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) × ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) ) ∈ ( Bnd ‘ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) )
75 39 74 syl3an1 ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑑 ∈ ℝ ) → ( 𝑀 ↾ ( ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) × ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) ) ∈ ( Bnd ‘ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) )
76 75 3expa ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃𝑋 ) ∧ 𝑑 ∈ ℝ ) → ( 𝑀 ↾ ( ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) × ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) ) ∈ ( Bnd ‘ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) )
77 76 adantrr ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃𝑋 ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) ) → ( 𝑀 ↾ ( ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) × ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) ) ∈ ( Bnd ‘ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) )
78 bndss ( ( ( 𝑀 ↾ ( ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) × ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) ) ∈ ( Bnd ‘ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) ∧ 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) → ( ( 𝑀 ↾ ( ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) × ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) ) ↾ ( 𝑌 × 𝑌 ) ) ∈ ( Bnd ‘ 𝑌 ) )
79 77 69 78 syl2anc ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃𝑋 ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) ) → ( ( 𝑀 ↾ ( ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) × ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) ) ↾ ( 𝑌 × 𝑌 ) ) ∈ ( Bnd ‘ 𝑌 ) )
80 73 79 eqeltrrd ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃𝑋 ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) ) → 𝑁 ∈ ( Bnd ‘ 𝑌 ) )
81 80 rexlimdvaa ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃𝑋 ) → ( ∃ 𝑑 ∈ ℝ 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) → 𝑁 ∈ ( Bnd ‘ 𝑌 ) ) )
82 68 81 impbid ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃𝑋 ) → ( 𝑁 ∈ ( Bnd ‘ 𝑌 ) ↔ ∃ 𝑑 ∈ ℝ 𝑌 ⊆ ( 𝑃 ( ball ‘ 𝑀 ) 𝑑 ) ) )