Step | Hyp | Ref
| Expression |
1 | | 0re 9919 |
. . . . . . 7
⊢ 0 ∈
ℝ |
2 | 1 | ne0ii 3882 |
. . . . . 6
⊢ ℝ
≠ ∅ |
3 | | 0ss 3924 |
. . . . . . . 8
⊢ ∅
⊆ (𝑃(ball‘𝑀)𝑑) |
4 | | sseq1 3589 |
. . . . . . . 8
⊢ (𝑌 = ∅ → (𝑌 ⊆ (𝑃(ball‘𝑀)𝑑) ↔ ∅ ⊆ (𝑃(ball‘𝑀)𝑑))) |
5 | 3, 4 | mpbiri 247 |
. . . . . . 7
⊢ (𝑌 = ∅ → 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑)) |
6 | 5 | ralrimivw 2950 |
. . . . . 6
⊢ (𝑌 = ∅ → ∀𝑑 ∈ ℝ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑)) |
7 | | r19.2z 4012 |
. . . . . 6
⊢ ((ℝ
≠ ∅ ∧ ∀𝑑 ∈ ℝ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑)) → ∃𝑑 ∈ ℝ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑)) |
8 | 2, 6, 7 | sylancr 694 |
. . . . 5
⊢ (𝑌 = ∅ → ∃𝑑 ∈ ℝ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑)) |
9 | 8 | a1i 11 |
. . . 4
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (Bnd‘𝑌)) → (𝑌 = ∅ → ∃𝑑 ∈ ℝ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑))) |
10 | | isbnd2 32752 |
. . . . . 6
⊢ ((𝑁 ∈ (Bnd‘𝑌) ∧ 𝑌 ≠ ∅) ↔ (𝑁 ∈ (∞Met‘𝑌) ∧ ∃𝑦 ∈ 𝑌 ∃𝑟 ∈ ℝ+ 𝑌 = (𝑦(ball‘𝑁)𝑟))) |
11 | | simplll 794 |
. . . . . . . . . . . 12
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → 𝑀 ∈ (Met‘𝑋)) |
12 | | ssbnd.2 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑁 = (𝑀 ↾ (𝑌 × 𝑌)) |
13 | 12 | dmeqi 5247 |
. . . . . . . . . . . . . . . . . . . 20
⊢ dom 𝑁 = dom (𝑀 ↾ (𝑌 × 𝑌)) |
14 | | dmres 5339 |
. . . . . . . . . . . . . . . . . . . 20
⊢ dom
(𝑀 ↾ (𝑌 × 𝑌)) = ((𝑌 × 𝑌) ∩ dom 𝑀) |
15 | 13, 14 | eqtri 2632 |
. . . . . . . . . . . . . . . . . . 19
⊢ dom 𝑁 = ((𝑌 × 𝑌) ∩ dom 𝑀) |
16 | | xmetf 21944 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ (∞Met‘𝑌) → 𝑁:(𝑌 × 𝑌)⟶ℝ*) |
17 | | fdm 5964 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁:(𝑌 × 𝑌)⟶ℝ* → dom
𝑁 = (𝑌 × 𝑌)) |
18 | 16, 17 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ (∞Met‘𝑌) → dom 𝑁 = (𝑌 × 𝑌)) |
19 | 15, 18 | syl5eqr 2658 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ (∞Met‘𝑌) → ((𝑌 × 𝑌) ∩ dom 𝑀) = (𝑌 × 𝑌)) |
20 | | df-ss 3554 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑌 × 𝑌) ⊆ dom 𝑀 ↔ ((𝑌 × 𝑌) ∩ dom 𝑀) = (𝑌 × 𝑌)) |
21 | 19, 20 | sylibr 223 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ (∞Met‘𝑌) → (𝑌 × 𝑌) ⊆ dom 𝑀) |
22 | 21 | ad2antlr 759 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → (𝑌 × 𝑌) ⊆ dom 𝑀) |
23 | | metf 21945 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑀 ∈ (Met‘𝑋) → 𝑀:(𝑋 × 𝑋)⟶ℝ) |
24 | | fdm 5964 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑀:(𝑋 × 𝑋)⟶ℝ → dom 𝑀 = (𝑋 × 𝑋)) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ (Met‘𝑋) → dom 𝑀 = (𝑋 × 𝑋)) |
26 | 25 | ad3antrrr 762 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → dom
𝑀 = (𝑋 × 𝑋)) |
27 | 22, 26 | sseqtrd 3604 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → (𝑌 × 𝑌) ⊆ (𝑋 × 𝑋)) |
28 | | dmss 5245 |
. . . . . . . . . . . . . . 15
⊢ ((𝑌 × 𝑌) ⊆ (𝑋 × 𝑋) → dom (𝑌 × 𝑌) ⊆ dom (𝑋 × 𝑋)) |
29 | 27, 28 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → dom
(𝑌 × 𝑌) ⊆ dom (𝑋 × 𝑋)) |
30 | | dmxpid 5266 |
. . . . . . . . . . . . . 14
⊢ dom
(𝑌 × 𝑌) = 𝑌 |
31 | | dmxpid 5266 |
. . . . . . . . . . . . . 14
⊢ dom
(𝑋 × 𝑋) = 𝑋 |
32 | 29, 30, 31 | 3sstr3g 3608 |
. . . . . . . . . . . . 13
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → 𝑌 ⊆ 𝑋) |
33 | | simprl 790 |
. . . . . . . . . . . . 13
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → 𝑦 ∈ 𝑌) |
34 | 32, 33 | sseldd 3569 |
. . . . . . . . . . . 12
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → 𝑦 ∈ 𝑋) |
35 | | simpllr 795 |
. . . . . . . . . . . 12
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → 𝑃 ∈ 𝑋) |
36 | | metcl 21947 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝑦𝑀𝑃) ∈ ℝ) |
37 | 11, 34, 35, 36 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → (𝑦𝑀𝑃) ∈ ℝ) |
38 | | rpre 11715 |
. . . . . . . . . . . 12
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ) |
39 | 38 | ad2antll 761 |
. . . . . . . . . . 11
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → 𝑟 ∈
ℝ) |
40 | 37, 39 | readdcld 9948 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → ((𝑦𝑀𝑃) + 𝑟) ∈ ℝ) |
41 | | metxmet 21949 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ (Met‘𝑋) → 𝑀 ∈ (∞Met‘𝑋)) |
42 | 11, 41 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → 𝑀 ∈ (∞Met‘𝑋)) |
43 | 34, 33 | elind 3760 |
. . . . . . . . . . . 12
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → 𝑦 ∈ (𝑋 ∩ 𝑌)) |
44 | | rpxr 11716 |
. . . . . . . . . . . . 13
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ*) |
45 | 44 | ad2antll 761 |
. . . . . . . . . . . 12
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → 𝑟 ∈
ℝ*) |
46 | 12 | blres 22046 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ (𝑋 ∩ 𝑌) ∧ 𝑟 ∈ ℝ*) → (𝑦(ball‘𝑁)𝑟) = ((𝑦(ball‘𝑀)𝑟) ∩ 𝑌)) |
47 | 42, 43, 45, 46 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → (𝑦(ball‘𝑁)𝑟) = ((𝑦(ball‘𝑀)𝑟) ∩ 𝑌)) |
48 | | inss1 3795 |
. . . . . . . . . . . 12
⊢ ((𝑦(ball‘𝑀)𝑟) ∩ 𝑌) ⊆ (𝑦(ball‘𝑀)𝑟) |
49 | 37 | leidd 10473 |
. . . . . . . . . . . . . 14
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → (𝑦𝑀𝑃) ≤ (𝑦𝑀𝑃)) |
50 | 37 | recnd 9947 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → (𝑦𝑀𝑃) ∈ ℂ) |
51 | 39 | recnd 9947 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → 𝑟 ∈
ℂ) |
52 | 50, 51 | pncand 10272 |
. . . . . . . . . . . . . 14
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → (((𝑦𝑀𝑃) + 𝑟) − 𝑟) = (𝑦𝑀𝑃)) |
53 | 49, 52 | breqtrrd 4611 |
. . . . . . . . . . . . 13
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → (𝑦𝑀𝑃) ≤ (((𝑦𝑀𝑃) + 𝑟) − 𝑟)) |
54 | | blss2 22019 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) ∧ (𝑟 ∈ ℝ ∧ ((𝑦𝑀𝑃) + 𝑟) ∈ ℝ ∧ (𝑦𝑀𝑃) ≤ (((𝑦𝑀𝑃) + 𝑟) − 𝑟))) → (𝑦(ball‘𝑀)𝑟) ⊆ (𝑃(ball‘𝑀)((𝑦𝑀𝑃) + 𝑟))) |
55 | 42, 34, 35, 39, 40, 53, 54 | syl33anc 1333 |
. . . . . . . . . . . 12
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → (𝑦(ball‘𝑀)𝑟) ⊆ (𝑃(ball‘𝑀)((𝑦𝑀𝑃) + 𝑟))) |
56 | 48, 55 | syl5ss 3579 |
. . . . . . . . . . 11
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → ((𝑦(ball‘𝑀)𝑟) ∩ 𝑌) ⊆ (𝑃(ball‘𝑀)((𝑦𝑀𝑃) + 𝑟))) |
57 | 47, 56 | eqsstrd 3602 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → (𝑦(ball‘𝑁)𝑟) ⊆ (𝑃(ball‘𝑀)((𝑦𝑀𝑃) + 𝑟))) |
58 | | oveq2 6557 |
. . . . . . . . . . . 12
⊢ (𝑑 = ((𝑦𝑀𝑃) + 𝑟) → (𝑃(ball‘𝑀)𝑑) = (𝑃(ball‘𝑀)((𝑦𝑀𝑃) + 𝑟))) |
59 | 58 | sseq2d 3596 |
. . . . . . . . . . 11
⊢ (𝑑 = ((𝑦𝑀𝑃) + 𝑟) → ((𝑦(ball‘𝑁)𝑟) ⊆ (𝑃(ball‘𝑀)𝑑) ↔ (𝑦(ball‘𝑁)𝑟) ⊆ (𝑃(ball‘𝑀)((𝑦𝑀𝑃) + 𝑟)))) |
60 | 59 | rspcev 3282 |
. . . . . . . . . 10
⊢ ((((𝑦𝑀𝑃) + 𝑟) ∈ ℝ ∧ (𝑦(ball‘𝑁)𝑟) ⊆ (𝑃(ball‘𝑀)((𝑦𝑀𝑃) + 𝑟))) → ∃𝑑 ∈ ℝ (𝑦(ball‘𝑁)𝑟) ⊆ (𝑃(ball‘𝑀)𝑑)) |
61 | 40, 57, 60 | syl2anc 691 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) →
∃𝑑 ∈ ℝ
(𝑦(ball‘𝑁)𝑟) ⊆ (𝑃(ball‘𝑀)𝑑)) |
62 | | sseq1 3589 |
. . . . . . . . . 10
⊢ (𝑌 = (𝑦(ball‘𝑁)𝑟) → (𝑌 ⊆ (𝑃(ball‘𝑀)𝑑) ↔ (𝑦(ball‘𝑁)𝑟) ⊆ (𝑃(ball‘𝑀)𝑑))) |
63 | 62 | rexbidv 3034 |
. . . . . . . . 9
⊢ (𝑌 = (𝑦(ball‘𝑁)𝑟) → (∃𝑑 ∈ ℝ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑) ↔ ∃𝑑 ∈ ℝ (𝑦(ball‘𝑁)𝑟) ⊆ (𝑃(ball‘𝑀)𝑑))) |
64 | 61, 63 | syl5ibrcom 236 |
. . . . . . . 8
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → (𝑌 = (𝑦(ball‘𝑁)𝑟) → ∃𝑑 ∈ ℝ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑))) |
65 | 64 | rexlimdvva 3020 |
. . . . . . 7
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) → (∃𝑦 ∈ 𝑌 ∃𝑟 ∈ ℝ+ 𝑌 = (𝑦(ball‘𝑁)𝑟) → ∃𝑑 ∈ ℝ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑))) |
66 | 65 | expimpd 627 |
. . . . . 6
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) → ((𝑁 ∈ (∞Met‘𝑌) ∧ ∃𝑦 ∈ 𝑌 ∃𝑟 ∈ ℝ+ 𝑌 = (𝑦(ball‘𝑁)𝑟)) → ∃𝑑 ∈ ℝ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑))) |
67 | 10, 66 | syl5bi 231 |
. . . . 5
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) → ((𝑁 ∈ (Bnd‘𝑌) ∧ 𝑌 ≠ ∅) → ∃𝑑 ∈ ℝ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑))) |
68 | 67 | expdimp 452 |
. . . 4
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (Bnd‘𝑌)) → (𝑌 ≠ ∅ → ∃𝑑 ∈ ℝ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑))) |
69 | 9, 68 | pm2.61dne 2868 |
. . 3
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (Bnd‘𝑌)) → ∃𝑑 ∈ ℝ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑)) |
70 | 69 | ex 449 |
. 2
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) → (𝑁 ∈ (Bnd‘𝑌) → ∃𝑑 ∈ ℝ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑))) |
71 | | simprr 792 |
. . . . . . 7
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑑 ∈ ℝ ∧ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑))) → 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑)) |
72 | | xpss12 5148 |
. . . . . . 7
⊢ ((𝑌 ⊆ (𝑃(ball‘𝑀)𝑑) ∧ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑)) → (𝑌 × 𝑌) ⊆ ((𝑃(ball‘𝑀)𝑑) × (𝑃(ball‘𝑀)𝑑))) |
73 | 71, 71, 72 | syl2anc 691 |
. . . . . 6
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑑 ∈ ℝ ∧ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑))) → (𝑌 × 𝑌) ⊆ ((𝑃(ball‘𝑀)𝑑) × (𝑃(ball‘𝑀)𝑑))) |
74 | 73 | resabs1d 5348 |
. . . . 5
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑑 ∈ ℝ ∧ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑))) → ((𝑀 ↾ ((𝑃(ball‘𝑀)𝑑) × (𝑃(ball‘𝑀)𝑑))) ↾ (𝑌 × 𝑌)) = (𝑀 ↾ (𝑌 × 𝑌))) |
75 | 74, 12 | syl6eqr 2662 |
. . . 4
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑑 ∈ ℝ ∧ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑))) → ((𝑀 ↾ ((𝑃(ball‘𝑀)𝑑) × (𝑃(ball‘𝑀)𝑑))) ↾ (𝑌 × 𝑌)) = 𝑁) |
76 | | blbnd 32756 |
. . . . . . . 8
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑑 ∈ ℝ) → (𝑀 ↾ ((𝑃(ball‘𝑀)𝑑) × (𝑃(ball‘𝑀)𝑑))) ∈ (Bnd‘(𝑃(ball‘𝑀)𝑑))) |
77 | 41, 76 | syl3an1 1351 |
. . . . . . 7
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑑 ∈ ℝ) → (𝑀 ↾ ((𝑃(ball‘𝑀)𝑑) × (𝑃(ball‘𝑀)𝑑))) ∈ (Bnd‘(𝑃(ball‘𝑀)𝑑))) |
78 | 77 | 3expa 1257 |
. . . . . 6
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑑 ∈ ℝ) → (𝑀 ↾ ((𝑃(ball‘𝑀)𝑑) × (𝑃(ball‘𝑀)𝑑))) ∈ (Bnd‘(𝑃(ball‘𝑀)𝑑))) |
79 | 78 | adantrr 749 |
. . . . 5
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑑 ∈ ℝ ∧ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑))) → (𝑀 ↾ ((𝑃(ball‘𝑀)𝑑) × (𝑃(ball‘𝑀)𝑑))) ∈ (Bnd‘(𝑃(ball‘𝑀)𝑑))) |
80 | | bndss 32755 |
. . . . 5
⊢ (((𝑀 ↾ ((𝑃(ball‘𝑀)𝑑) × (𝑃(ball‘𝑀)𝑑))) ∈ (Bnd‘(𝑃(ball‘𝑀)𝑑)) ∧ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑)) → ((𝑀 ↾ ((𝑃(ball‘𝑀)𝑑) × (𝑃(ball‘𝑀)𝑑))) ↾ (𝑌 × 𝑌)) ∈ (Bnd‘𝑌)) |
81 | 79, 71, 80 | syl2anc 691 |
. . . 4
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑑 ∈ ℝ ∧ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑))) → ((𝑀 ↾ ((𝑃(ball‘𝑀)𝑑) × (𝑃(ball‘𝑀)𝑑))) ↾ (𝑌 × 𝑌)) ∈ (Bnd‘𝑌)) |
82 | 75, 81 | eqeltrrd 2689 |
. . 3
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑑 ∈ ℝ ∧ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑))) → 𝑁 ∈ (Bnd‘𝑌)) |
83 | 82 | rexlimdvaa 3014 |
. 2
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) → (∃𝑑 ∈ ℝ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑) → 𝑁 ∈ (Bnd‘𝑌))) |
84 | 70, 83 | impbid 201 |
1
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) → (𝑁 ∈ (Bnd‘𝑌) ↔ ∃𝑑 ∈ ℝ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑))) |