Step | Hyp | Ref
| Expression |
1 | | 0re 10924 |
. . . . . . 7
⊢ 0 ∈
ℝ |
2 | 1 | ne0ii 4273 |
. . . . . 6
⊢ ℝ
≠ ∅ |
3 | | 0ss 4332 |
. . . . . . . 8
⊢ ∅
⊆ (𝑃(ball‘𝑀)𝑑) |
4 | | sseq1 3947 |
. . . . . . . 8
⊢ (𝑌 = ∅ → (𝑌 ⊆ (𝑃(ball‘𝑀)𝑑) ↔ ∅ ⊆ (𝑃(ball‘𝑀)𝑑))) |
5 | 3, 4 | mpbiri 257 |
. . . . . . 7
⊢ (𝑌 = ∅ → 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑)) |
6 | 5 | ralrimivw 3107 |
. . . . . 6
⊢ (𝑌 = ∅ → ∀𝑑 ∈ ℝ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑)) |
7 | | r19.2z 4427 |
. . . . . 6
⊢ ((ℝ
≠ ∅ ∧ ∀𝑑 ∈ ℝ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑)) → ∃𝑑 ∈ ℝ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑)) |
8 | 2, 6, 7 | sylancr 586 |
. . . . 5
⊢ (𝑌 = ∅ → ∃𝑑 ∈ ℝ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑)) |
9 | 8 | a1i 11 |
. . . 4
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (Bnd‘𝑌)) → (𝑌 = ∅ → ∃𝑑 ∈ ℝ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑))) |
10 | | isbnd2 35910 |
. . . . . 6
⊢ ((𝑁 ∈ (Bnd‘𝑌) ∧ 𝑌 ≠ ∅) ↔ (𝑁 ∈ (∞Met‘𝑌) ∧ ∃𝑦 ∈ 𝑌 ∃𝑟 ∈ ℝ+ 𝑌 = (𝑦(ball‘𝑁)𝑟))) |
11 | | simplll 771 |
. . . . . . . . . . . 12
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → 𝑀 ∈ (Met‘𝑋)) |
12 | | ssbnd.2 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑁 = (𝑀 ↾ (𝑌 × 𝑌)) |
13 | 12 | dmeqi 5807 |
. . . . . . . . . . . . . . . . . . . 20
⊢ dom 𝑁 = dom (𝑀 ↾ (𝑌 × 𝑌)) |
14 | | dmres 5907 |
. . . . . . . . . . . . . . . . . . . 20
⊢ dom
(𝑀 ↾ (𝑌 × 𝑌)) = ((𝑌 × 𝑌) ∩ dom 𝑀) |
15 | 13, 14 | eqtri 2765 |
. . . . . . . . . . . . . . . . . . 19
⊢ dom 𝑁 = ((𝑌 × 𝑌) ∩ dom 𝑀) |
16 | | xmetf 23426 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ (∞Met‘𝑌) → 𝑁:(𝑌 × 𝑌)⟶ℝ*) |
17 | 16 | fdmd 6600 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ (∞Met‘𝑌) → dom 𝑁 = (𝑌 × 𝑌)) |
18 | 15, 17 | eqtr3id 2791 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ (∞Met‘𝑌) → ((𝑌 × 𝑌) ∩ dom 𝑀) = (𝑌 × 𝑌)) |
19 | | df-ss 3905 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑌 × 𝑌) ⊆ dom 𝑀 ↔ ((𝑌 × 𝑌) ∩ dom 𝑀) = (𝑌 × 𝑌)) |
20 | 18, 19 | sylibr 233 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ (∞Met‘𝑌) → (𝑌 × 𝑌) ⊆ dom 𝑀) |
21 | 20 | ad2antlr 723 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → (𝑌 × 𝑌) ⊆ dom 𝑀) |
22 | | metf 23427 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑀 ∈ (Met‘𝑋) → 𝑀:(𝑋 × 𝑋)⟶ℝ) |
23 | 22 | fdmd 6600 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ (Met‘𝑋) → dom 𝑀 = (𝑋 × 𝑋)) |
24 | 23 | ad3antrrr 726 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → dom
𝑀 = (𝑋 × 𝑋)) |
25 | 21, 24 | sseqtrd 3962 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → (𝑌 × 𝑌) ⊆ (𝑋 × 𝑋)) |
26 | | dmss 5805 |
. . . . . . . . . . . . . . 15
⊢ ((𝑌 × 𝑌) ⊆ (𝑋 × 𝑋) → dom (𝑌 × 𝑌) ⊆ dom (𝑋 × 𝑋)) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → dom
(𝑌 × 𝑌) ⊆ dom (𝑋 × 𝑋)) |
28 | | dmxpid 5833 |
. . . . . . . . . . . . . 14
⊢ dom
(𝑌 × 𝑌) = 𝑌 |
29 | | dmxpid 5833 |
. . . . . . . . . . . . . 14
⊢ dom
(𝑋 × 𝑋) = 𝑋 |
30 | 27, 28, 29 | 3sstr3g 3966 |
. . . . . . . . . . . . 13
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → 𝑌 ⊆ 𝑋) |
31 | | simprl 767 |
. . . . . . . . . . . . 13
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → 𝑦 ∈ 𝑌) |
32 | 30, 31 | sseldd 3923 |
. . . . . . . . . . . 12
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → 𝑦 ∈ 𝑋) |
33 | | simpllr 772 |
. . . . . . . . . . . 12
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → 𝑃 ∈ 𝑋) |
34 | | metcl 23429 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝑦𝑀𝑃) ∈ ℝ) |
35 | 11, 32, 33, 34 | syl3anc 1369 |
. . . . . . . . . . 11
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → (𝑦𝑀𝑃) ∈ ℝ) |
36 | | rpre 12683 |
. . . . . . . . . . . 12
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ) |
37 | 36 | ad2antll 725 |
. . . . . . . . . . 11
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → 𝑟 ∈
ℝ) |
38 | 35, 37 | readdcld 10951 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → ((𝑦𝑀𝑃) + 𝑟) ∈ ℝ) |
39 | | metxmet 23431 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ (Met‘𝑋) → 𝑀 ∈ (∞Met‘𝑋)) |
40 | 11, 39 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → 𝑀 ∈ (∞Met‘𝑋)) |
41 | 32, 31 | elind 4129 |
. . . . . . . . . . . 12
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → 𝑦 ∈ (𝑋 ∩ 𝑌)) |
42 | | rpxr 12684 |
. . . . . . . . . . . . 13
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ*) |
43 | 42 | ad2antll 725 |
. . . . . . . . . . . 12
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → 𝑟 ∈
ℝ*) |
44 | 12 | blres 23528 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ (𝑋 ∩ 𝑌) ∧ 𝑟 ∈ ℝ*) → (𝑦(ball‘𝑁)𝑟) = ((𝑦(ball‘𝑀)𝑟) ∩ 𝑌)) |
45 | 40, 41, 43, 44 | syl3anc 1369 |
. . . . . . . . . . 11
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → (𝑦(ball‘𝑁)𝑟) = ((𝑦(ball‘𝑀)𝑟) ∩ 𝑌)) |
46 | | inss1 4164 |
. . . . . . . . . . . 12
⊢ ((𝑦(ball‘𝑀)𝑟) ∩ 𝑌) ⊆ (𝑦(ball‘𝑀)𝑟) |
47 | 35 | leidd 11487 |
. . . . . . . . . . . . . 14
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → (𝑦𝑀𝑃) ≤ (𝑦𝑀𝑃)) |
48 | 35 | recnd 10950 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → (𝑦𝑀𝑃) ∈ ℂ) |
49 | 37 | recnd 10950 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → 𝑟 ∈
ℂ) |
50 | 48, 49 | pncand 11279 |
. . . . . . . . . . . . . 14
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → (((𝑦𝑀𝑃) + 𝑟) − 𝑟) = (𝑦𝑀𝑃)) |
51 | 47, 50 | breqtrrd 5103 |
. . . . . . . . . . . . 13
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → (𝑦𝑀𝑃) ≤ (((𝑦𝑀𝑃) + 𝑟) − 𝑟)) |
52 | | blss2 23501 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) ∧ (𝑟 ∈ ℝ ∧ ((𝑦𝑀𝑃) + 𝑟) ∈ ℝ ∧ (𝑦𝑀𝑃) ≤ (((𝑦𝑀𝑃) + 𝑟) − 𝑟))) → (𝑦(ball‘𝑀)𝑟) ⊆ (𝑃(ball‘𝑀)((𝑦𝑀𝑃) + 𝑟))) |
53 | 40, 32, 33, 37, 38, 51, 52 | syl33anc 1383 |
. . . . . . . . . . . 12
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → (𝑦(ball‘𝑀)𝑟) ⊆ (𝑃(ball‘𝑀)((𝑦𝑀𝑃) + 𝑟))) |
54 | 46, 53 | sstrid 3933 |
. . . . . . . . . . 11
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → ((𝑦(ball‘𝑀)𝑟) ∩ 𝑌) ⊆ (𝑃(ball‘𝑀)((𝑦𝑀𝑃) + 𝑟))) |
55 | 45, 54 | eqsstrd 3960 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → (𝑦(ball‘𝑁)𝑟) ⊆ (𝑃(ball‘𝑀)((𝑦𝑀𝑃) + 𝑟))) |
56 | | oveq2 7268 |
. . . . . . . . . . . 12
⊢ (𝑑 = ((𝑦𝑀𝑃) + 𝑟) → (𝑃(ball‘𝑀)𝑑) = (𝑃(ball‘𝑀)((𝑦𝑀𝑃) + 𝑟))) |
57 | 56 | sseq2d 3954 |
. . . . . . . . . . 11
⊢ (𝑑 = ((𝑦𝑀𝑃) + 𝑟) → ((𝑦(ball‘𝑁)𝑟) ⊆ (𝑃(ball‘𝑀)𝑑) ↔ (𝑦(ball‘𝑁)𝑟) ⊆ (𝑃(ball‘𝑀)((𝑦𝑀𝑃) + 𝑟)))) |
58 | 57 | rspcev 3557 |
. . . . . . . . . 10
⊢ ((((𝑦𝑀𝑃) + 𝑟) ∈ ℝ ∧ (𝑦(ball‘𝑁)𝑟) ⊆ (𝑃(ball‘𝑀)((𝑦𝑀𝑃) + 𝑟))) → ∃𝑑 ∈ ℝ (𝑦(ball‘𝑁)𝑟) ⊆ (𝑃(ball‘𝑀)𝑑)) |
59 | 38, 55, 58 | syl2anc 583 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) →
∃𝑑 ∈ ℝ
(𝑦(ball‘𝑁)𝑟) ⊆ (𝑃(ball‘𝑀)𝑑)) |
60 | | sseq1 3947 |
. . . . . . . . . 10
⊢ (𝑌 = (𝑦(ball‘𝑁)𝑟) → (𝑌 ⊆ (𝑃(ball‘𝑀)𝑑) ↔ (𝑦(ball‘𝑁)𝑟) ⊆ (𝑃(ball‘𝑀)𝑑))) |
61 | 60 | rexbidv 3224 |
. . . . . . . . 9
⊢ (𝑌 = (𝑦(ball‘𝑁)𝑟) → (∃𝑑 ∈ ℝ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑) ↔ ∃𝑑 ∈ ℝ (𝑦(ball‘𝑁)𝑟) ⊆ (𝑃(ball‘𝑀)𝑑))) |
62 | 59, 61 | syl5ibrcom 246 |
. . . . . . . 8
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → (𝑌 = (𝑦(ball‘𝑁)𝑟) → ∃𝑑 ∈ ℝ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑))) |
63 | 62 | rexlimdvva 3221 |
. . . . . . 7
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) → (∃𝑦 ∈ 𝑌 ∃𝑟 ∈ ℝ+ 𝑌 = (𝑦(ball‘𝑁)𝑟) → ∃𝑑 ∈ ℝ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑))) |
64 | 63 | expimpd 453 |
. . . . . 6
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) → ((𝑁 ∈ (∞Met‘𝑌) ∧ ∃𝑦 ∈ 𝑌 ∃𝑟 ∈ ℝ+ 𝑌 = (𝑦(ball‘𝑁)𝑟)) → ∃𝑑 ∈ ℝ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑))) |
65 | 10, 64 | syl5bi 241 |
. . . . 5
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) → ((𝑁 ∈ (Bnd‘𝑌) ∧ 𝑌 ≠ ∅) → ∃𝑑 ∈ ℝ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑))) |
66 | 65 | expdimp 452 |
. . . 4
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (Bnd‘𝑌)) → (𝑌 ≠ ∅ → ∃𝑑 ∈ ℝ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑))) |
67 | 9, 66 | pm2.61dne 3029 |
. . 3
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (Bnd‘𝑌)) → ∃𝑑 ∈ ℝ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑)) |
68 | 67 | ex 412 |
. 2
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) → (𝑁 ∈ (Bnd‘𝑌) → ∃𝑑 ∈ ℝ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑))) |
69 | | simprr 769 |
. . . . . . 7
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑑 ∈ ℝ ∧ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑))) → 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑)) |
70 | | xpss12 5600 |
. . . . . . 7
⊢ ((𝑌 ⊆ (𝑃(ball‘𝑀)𝑑) ∧ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑)) → (𝑌 × 𝑌) ⊆ ((𝑃(ball‘𝑀)𝑑) × (𝑃(ball‘𝑀)𝑑))) |
71 | 69, 69, 70 | syl2anc 583 |
. . . . . 6
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑑 ∈ ℝ ∧ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑))) → (𝑌 × 𝑌) ⊆ ((𝑃(ball‘𝑀)𝑑) × (𝑃(ball‘𝑀)𝑑))) |
72 | 71 | resabs1d 5916 |
. . . . 5
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑑 ∈ ℝ ∧ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑))) → ((𝑀 ↾ ((𝑃(ball‘𝑀)𝑑) × (𝑃(ball‘𝑀)𝑑))) ↾ (𝑌 × 𝑌)) = (𝑀 ↾ (𝑌 × 𝑌))) |
73 | 72, 12 | eqtr4di 2795 |
. . . 4
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑑 ∈ ℝ ∧ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑))) → ((𝑀 ↾ ((𝑃(ball‘𝑀)𝑑) × (𝑃(ball‘𝑀)𝑑))) ↾ (𝑌 × 𝑌)) = 𝑁) |
74 | | blbnd 35914 |
. . . . . . . 8
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑑 ∈ ℝ) → (𝑀 ↾ ((𝑃(ball‘𝑀)𝑑) × (𝑃(ball‘𝑀)𝑑))) ∈ (Bnd‘(𝑃(ball‘𝑀)𝑑))) |
75 | 39, 74 | syl3an1 1161 |
. . . . . . 7
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑑 ∈ ℝ) → (𝑀 ↾ ((𝑃(ball‘𝑀)𝑑) × (𝑃(ball‘𝑀)𝑑))) ∈ (Bnd‘(𝑃(ball‘𝑀)𝑑))) |
76 | 75 | 3expa 1116 |
. . . . . 6
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑑 ∈ ℝ) → (𝑀 ↾ ((𝑃(ball‘𝑀)𝑑) × (𝑃(ball‘𝑀)𝑑))) ∈ (Bnd‘(𝑃(ball‘𝑀)𝑑))) |
77 | 76 | adantrr 713 |
. . . . 5
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑑 ∈ ℝ ∧ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑))) → (𝑀 ↾ ((𝑃(ball‘𝑀)𝑑) × (𝑃(ball‘𝑀)𝑑))) ∈ (Bnd‘(𝑃(ball‘𝑀)𝑑))) |
78 | | bndss 35913 |
. . . . 5
⊢ (((𝑀 ↾ ((𝑃(ball‘𝑀)𝑑) × (𝑃(ball‘𝑀)𝑑))) ∈ (Bnd‘(𝑃(ball‘𝑀)𝑑)) ∧ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑)) → ((𝑀 ↾ ((𝑃(ball‘𝑀)𝑑) × (𝑃(ball‘𝑀)𝑑))) ↾ (𝑌 × 𝑌)) ∈ (Bnd‘𝑌)) |
79 | 77, 69, 78 | syl2anc 583 |
. . . 4
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑑 ∈ ℝ ∧ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑))) → ((𝑀 ↾ ((𝑃(ball‘𝑀)𝑑) × (𝑃(ball‘𝑀)𝑑))) ↾ (𝑌 × 𝑌)) ∈ (Bnd‘𝑌)) |
80 | 73, 79 | eqeltrrd 2838 |
. . 3
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑑 ∈ ℝ ∧ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑))) → 𝑁 ∈ (Bnd‘𝑌)) |
81 | 80 | rexlimdvaa 3212 |
. 2
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) → (∃𝑑 ∈ ℝ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑) → 𝑁 ∈ (Bnd‘𝑌))) |
82 | 68, 81 | impbid 211 |
1
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) → (𝑁 ∈ (Bnd‘𝑌) ↔ ∃𝑑 ∈ ℝ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑))) |