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
|
syl5eqr |
⊢ ( 𝑁 ∈ ( ∞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 ‘ 𝑀 ) 𝑑 ) ) ) |