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

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 dfss2 ⊢ ( ( 𝑌 × 𝑌 ) ⊆ 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 biimtrid ⊢ ( ( 𝑀 ∈ ( 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 ‘ 𝑀 ) 𝑑 ) ) )