| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 0re 11264 | . . . . . . 7
⊢ 0 ∈
ℝ | 
| 2 | 1 | ne0ii 4343 | . . . . . 6
⊢ ℝ
≠ ∅ | 
| 3 |  | 0ss 4399 | . . . . . . . 8
⊢ ∅
⊆ (𝑃(ball‘𝑀)𝑑) | 
| 4 |  | sseq1 4008 | . . . . . . . 8
⊢ (𝑌 = ∅ → (𝑌 ⊆ (𝑃(ball‘𝑀)𝑑) ↔ ∅ ⊆ (𝑃(ball‘𝑀)𝑑))) | 
| 5 | 3, 4 | mpbiri 258 | . . . . . . 7
⊢ (𝑌 = ∅ → 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑)) | 
| 6 | 5 | ralrimivw 3149 | . . . . . 6
⊢ (𝑌 = ∅ → ∀𝑑 ∈ ℝ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑)) | 
| 7 |  | r19.2z 4494 | . . . . . 6
⊢ ((ℝ
≠ ∅ ∧ ∀𝑑 ∈ ℝ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑)) → ∃𝑑 ∈ ℝ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑)) | 
| 8 | 2, 6, 7 | sylancr 587 | . . . . 5
⊢ (𝑌 = ∅ → ∃𝑑 ∈ ℝ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑)) | 
| 9 | 8 | a1i 11 | . . . 4
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (Bnd‘𝑌)) → (𝑌 = ∅ → ∃𝑑 ∈ ℝ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑))) | 
| 10 |  | isbnd2 37791 | . . . . . 6
⊢ ((𝑁 ∈ (Bnd‘𝑌) ∧ 𝑌 ≠ ∅) ↔ (𝑁 ∈ (∞Met‘𝑌) ∧ ∃𝑦 ∈ 𝑌 ∃𝑟 ∈ ℝ+ 𝑌 = (𝑦(ball‘𝑁)𝑟))) | 
| 11 |  | simplll 774 | . . . . . . . . . . . 12
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → 𝑀 ∈ (Met‘𝑋)) | 
| 12 |  | ssbnd.2 | . . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑁 = (𝑀 ↾ (𝑌 × 𝑌)) | 
| 13 | 12 | dmeqi 5914 | . . . . . . . . . . . . . . . . . . . 20
⊢ dom 𝑁 = dom (𝑀 ↾ (𝑌 × 𝑌)) | 
| 14 |  | dmres 6029 | . . . . . . . . . . . . . . . . . . . 20
⊢ dom
(𝑀 ↾ (𝑌 × 𝑌)) = ((𝑌 × 𝑌) ∩ dom 𝑀) | 
| 15 | 13, 14 | eqtri 2764 | . . . . . . . . . . . . . . . . . . 19
⊢ dom 𝑁 = ((𝑌 × 𝑌) ∩ dom 𝑀) | 
| 16 |  | xmetf 24340 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ (∞Met‘𝑌) → 𝑁:(𝑌 × 𝑌)⟶ℝ*) | 
| 17 | 16 | fdmd 6745 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ (∞Met‘𝑌) → dom 𝑁 = (𝑌 × 𝑌)) | 
| 18 | 15, 17 | eqtr3id 2790 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ (∞Met‘𝑌) → ((𝑌 × 𝑌) ∩ dom 𝑀) = (𝑌 × 𝑌)) | 
| 19 |  | dfss2 3968 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑌 × 𝑌) ⊆ dom 𝑀 ↔ ((𝑌 × 𝑌) ∩ dom 𝑀) = (𝑌 × 𝑌)) | 
| 20 | 18, 19 | sylibr 234 | . . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ (∞Met‘𝑌) → (𝑌 × 𝑌) ⊆ dom 𝑀) | 
| 21 | 20 | ad2antlr 727 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → (𝑌 × 𝑌) ⊆ dom 𝑀) | 
| 22 |  | metf 24341 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑀 ∈ (Met‘𝑋) → 𝑀:(𝑋 × 𝑋)⟶ℝ) | 
| 23 | 22 | fdmd 6745 | . . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ (Met‘𝑋) → dom 𝑀 = (𝑋 × 𝑋)) | 
| 24 | 23 | ad3antrrr 730 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → dom
𝑀 = (𝑋 × 𝑋)) | 
| 25 | 21, 24 | sseqtrd 4019 | . . . . . . . . . . . . . . 15
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → (𝑌 × 𝑌) ⊆ (𝑋 × 𝑋)) | 
| 26 |  | dmss 5912 | . . . . . . . . . . . . . . 15
⊢ ((𝑌 × 𝑌) ⊆ (𝑋 × 𝑋) → dom (𝑌 × 𝑌) ⊆ dom (𝑋 × 𝑋)) | 
| 27 | 25, 26 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → dom
(𝑌 × 𝑌) ⊆ dom (𝑋 × 𝑋)) | 
| 28 |  | dmxpid 5940 | . . . . . . . . . . . . . 14
⊢ dom
(𝑌 × 𝑌) = 𝑌 | 
| 29 |  | dmxpid 5940 | . . . . . . . . . . . . . 14
⊢ dom
(𝑋 × 𝑋) = 𝑋 | 
| 30 | 27, 28, 29 | 3sstr3g 4035 | . . . . . . . . . . . . 13
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → 𝑌 ⊆ 𝑋) | 
| 31 |  | simprl 770 | . . . . . . . . . . . . 13
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → 𝑦 ∈ 𝑌) | 
| 32 | 30, 31 | sseldd 3983 | . . . . . . . . . . . 12
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → 𝑦 ∈ 𝑋) | 
| 33 |  | simpllr 775 | . . . . . . . . . . . 12
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → 𝑃 ∈ 𝑋) | 
| 34 |  | metcl 24343 | . . . . . . . . . . . 12
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝑦𝑀𝑃) ∈ ℝ) | 
| 35 | 11, 32, 33, 34 | syl3anc 1372 | . . . . . . . . . . 11
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → (𝑦𝑀𝑃) ∈ ℝ) | 
| 36 |  | rpre 13044 | . . . . . . . . . . . 12
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ) | 
| 37 | 36 | ad2antll 729 | . . . . . . . . . . 11
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → 𝑟 ∈
ℝ) | 
| 38 | 35, 37 | readdcld 11291 | . . . . . . . . . 10
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → ((𝑦𝑀𝑃) + 𝑟) ∈ ℝ) | 
| 39 |  | metxmet 24345 | . . . . . . . . . . . . 13
⊢ (𝑀 ∈ (Met‘𝑋) → 𝑀 ∈ (∞Met‘𝑋)) | 
| 40 | 11, 39 | syl 17 | . . . . . . . . . . . 12
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → 𝑀 ∈ (∞Met‘𝑋)) | 
| 41 | 32, 31 | elind 4199 | . . . . . . . . . . . 12
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → 𝑦 ∈ (𝑋 ∩ 𝑌)) | 
| 42 |  | rpxr 13045 | . . . . . . . . . . . . 13
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ*) | 
| 43 | 42 | ad2antll 729 | . . . . . . . . . . . 12
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → 𝑟 ∈
ℝ*) | 
| 44 | 12 | blres 24442 | . . . . . . . . . . . 12
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ (𝑋 ∩ 𝑌) ∧ 𝑟 ∈ ℝ*) → (𝑦(ball‘𝑁)𝑟) = ((𝑦(ball‘𝑀)𝑟) ∩ 𝑌)) | 
| 45 | 40, 41, 43, 44 | syl3anc 1372 | . . . . . . . . . . 11
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → (𝑦(ball‘𝑁)𝑟) = ((𝑦(ball‘𝑀)𝑟) ∩ 𝑌)) | 
| 46 |  | inss1 4236 | . . . . . . . . . . . 12
⊢ ((𝑦(ball‘𝑀)𝑟) ∩ 𝑌) ⊆ (𝑦(ball‘𝑀)𝑟) | 
| 47 | 35 | leidd 11830 | . . . . . . . . . . . . . 14
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → (𝑦𝑀𝑃) ≤ (𝑦𝑀𝑃)) | 
| 48 | 35 | recnd 11290 | . . . . . . . . . . . . . . 15
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → (𝑦𝑀𝑃) ∈ ℂ) | 
| 49 | 37 | recnd 11290 | . . . . . . . . . . . . . . 15
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → 𝑟 ∈
ℂ) | 
| 50 | 48, 49 | pncand 11622 | . . . . . . . . . . . . . 14
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → (((𝑦𝑀𝑃) + 𝑟) − 𝑟) = (𝑦𝑀𝑃)) | 
| 51 | 47, 50 | breqtrrd 5170 | . . . . . . . . . . . . 13
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → (𝑦𝑀𝑃) ≤ (((𝑦𝑀𝑃) + 𝑟) − 𝑟)) | 
| 52 |  | blss2 24415 | . . . . . . . . . . . . 13
⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) ∧ (𝑟 ∈ ℝ ∧ ((𝑦𝑀𝑃) + 𝑟) ∈ ℝ ∧ (𝑦𝑀𝑃) ≤ (((𝑦𝑀𝑃) + 𝑟) − 𝑟))) → (𝑦(ball‘𝑀)𝑟) ⊆ (𝑃(ball‘𝑀)((𝑦𝑀𝑃) + 𝑟))) | 
| 53 | 40, 32, 33, 37, 38, 51, 52 | syl33anc 1386 | . . . . . . . . . . . 12
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → (𝑦(ball‘𝑀)𝑟) ⊆ (𝑃(ball‘𝑀)((𝑦𝑀𝑃) + 𝑟))) | 
| 54 | 46, 53 | sstrid 3994 | . . . . . . . . . . 11
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → ((𝑦(ball‘𝑀)𝑟) ∩ 𝑌) ⊆ (𝑃(ball‘𝑀)((𝑦𝑀𝑃) + 𝑟))) | 
| 55 | 45, 54 | eqsstrd 4017 | . . . . . . . . . 10
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → (𝑦(ball‘𝑁)𝑟) ⊆ (𝑃(ball‘𝑀)((𝑦𝑀𝑃) + 𝑟))) | 
| 56 |  | oveq2 7440 | . . . . . . . . . . . 12
⊢ (𝑑 = ((𝑦𝑀𝑃) + 𝑟) → (𝑃(ball‘𝑀)𝑑) = (𝑃(ball‘𝑀)((𝑦𝑀𝑃) + 𝑟))) | 
| 57 | 56 | sseq2d 4015 | . . . . . . . . . . 11
⊢ (𝑑 = ((𝑦𝑀𝑃) + 𝑟) → ((𝑦(ball‘𝑁)𝑟) ⊆ (𝑃(ball‘𝑀)𝑑) ↔ (𝑦(ball‘𝑁)𝑟) ⊆ (𝑃(ball‘𝑀)((𝑦𝑀𝑃) + 𝑟)))) | 
| 58 | 57 | rspcev 3621 | . . . . . . . . . 10
⊢ ((((𝑦𝑀𝑃) + 𝑟) ∈ ℝ ∧ (𝑦(ball‘𝑁)𝑟) ⊆ (𝑃(ball‘𝑀)((𝑦𝑀𝑃) + 𝑟))) → ∃𝑑 ∈ ℝ (𝑦(ball‘𝑁)𝑟) ⊆ (𝑃(ball‘𝑀)𝑑)) | 
| 59 | 38, 55, 58 | syl2anc 584 | . . . . . . . . 9
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) →
∃𝑑 ∈ ℝ
(𝑦(ball‘𝑁)𝑟) ⊆ (𝑃(ball‘𝑀)𝑑)) | 
| 60 |  | sseq1 4008 | . . . . . . . . . 10
⊢ (𝑌 = (𝑦(ball‘𝑁)𝑟) → (𝑌 ⊆ (𝑃(ball‘𝑀)𝑑) ↔ (𝑦(ball‘𝑁)𝑟) ⊆ (𝑃(ball‘𝑀)𝑑))) | 
| 61 | 60 | rexbidv 3178 | . . . . . . . . 9
⊢ (𝑌 = (𝑦(ball‘𝑁)𝑟) → (∃𝑑 ∈ ℝ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑) ↔ ∃𝑑 ∈ ℝ (𝑦(ball‘𝑁)𝑟) ⊆ (𝑃(ball‘𝑀)𝑑))) | 
| 62 | 59, 61 | syl5ibrcom 247 | . . . . . . . 8
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑦 ∈ 𝑌 ∧ 𝑟 ∈ ℝ+)) → (𝑌 = (𝑦(ball‘𝑁)𝑟) → ∃𝑑 ∈ ℝ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑))) | 
| 63 | 62 | rexlimdvva 3212 | . . . . . . 7
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) → (∃𝑦 ∈ 𝑌 ∃𝑟 ∈ ℝ+ 𝑌 = (𝑦(ball‘𝑁)𝑟) → ∃𝑑 ∈ ℝ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑))) | 
| 64 | 63 | expimpd 453 | . . . . . 6
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) → ((𝑁 ∈ (∞Met‘𝑌) ∧ ∃𝑦 ∈ 𝑌 ∃𝑟 ∈ ℝ+ 𝑌 = (𝑦(ball‘𝑁)𝑟)) → ∃𝑑 ∈ ℝ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑))) | 
| 65 | 10, 64 | biimtrid 242 | . . . . 5
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) → ((𝑁 ∈ (Bnd‘𝑌) ∧ 𝑌 ≠ ∅) → ∃𝑑 ∈ ℝ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑))) | 
| 66 | 65 | expdimp 452 | . . . 4
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (Bnd‘𝑌)) → (𝑌 ≠ ∅ → ∃𝑑 ∈ ℝ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑))) | 
| 67 | 9, 66 | pm2.61dne 3027 | . . 3
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ (Bnd‘𝑌)) → ∃𝑑 ∈ ℝ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑)) | 
| 68 | 67 | ex 412 | . 2
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) → (𝑁 ∈ (Bnd‘𝑌) → ∃𝑑 ∈ ℝ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑))) | 
| 69 |  | simprr 772 | . . . . . . 7
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑑 ∈ ℝ ∧ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑))) → 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑)) | 
| 70 |  | xpss12 5699 | . . . . . . 7
⊢ ((𝑌 ⊆ (𝑃(ball‘𝑀)𝑑) ∧ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑)) → (𝑌 × 𝑌) ⊆ ((𝑃(ball‘𝑀)𝑑) × (𝑃(ball‘𝑀)𝑑))) | 
| 71 | 69, 69, 70 | syl2anc 584 | . . . . . 6
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑑 ∈ ℝ ∧ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑))) → (𝑌 × 𝑌) ⊆ ((𝑃(ball‘𝑀)𝑑) × (𝑃(ball‘𝑀)𝑑))) | 
| 72 | 71 | resabs1d 6025 | . . . . 5
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑑 ∈ ℝ ∧ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑))) → ((𝑀 ↾ ((𝑃(ball‘𝑀)𝑑) × (𝑃(ball‘𝑀)𝑑))) ↾ (𝑌 × 𝑌)) = (𝑀 ↾ (𝑌 × 𝑌))) | 
| 73 | 72, 12 | eqtr4di 2794 | . . . 4
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑑 ∈ ℝ ∧ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑))) → ((𝑀 ↾ ((𝑃(ball‘𝑀)𝑑) × (𝑃(ball‘𝑀)𝑑))) ↾ (𝑌 × 𝑌)) = 𝑁) | 
| 74 |  | blbnd 37795 | . . . . . . . 8
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑑 ∈ ℝ) → (𝑀 ↾ ((𝑃(ball‘𝑀)𝑑) × (𝑃(ball‘𝑀)𝑑))) ∈ (Bnd‘(𝑃(ball‘𝑀)𝑑))) | 
| 75 | 39, 74 | syl3an1 1163 | . . . . . . 7
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑑 ∈ ℝ) → (𝑀 ↾ ((𝑃(ball‘𝑀)𝑑) × (𝑃(ball‘𝑀)𝑑))) ∈ (Bnd‘(𝑃(ball‘𝑀)𝑑))) | 
| 76 | 75 | 3expa 1118 | . . . . . 6
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑑 ∈ ℝ) → (𝑀 ↾ ((𝑃(ball‘𝑀)𝑑) × (𝑃(ball‘𝑀)𝑑))) ∈ (Bnd‘(𝑃(ball‘𝑀)𝑑))) | 
| 77 | 76 | adantrr 717 | . . . . 5
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑑 ∈ ℝ ∧ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑))) → (𝑀 ↾ ((𝑃(ball‘𝑀)𝑑) × (𝑃(ball‘𝑀)𝑑))) ∈ (Bnd‘(𝑃(ball‘𝑀)𝑑))) | 
| 78 |  | bndss 37794 | . . . . 5
⊢ (((𝑀 ↾ ((𝑃(ball‘𝑀)𝑑) × (𝑃(ball‘𝑀)𝑑))) ∈ (Bnd‘(𝑃(ball‘𝑀)𝑑)) ∧ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑)) → ((𝑀 ↾ ((𝑃(ball‘𝑀)𝑑) × (𝑃(ball‘𝑀)𝑑))) ↾ (𝑌 × 𝑌)) ∈ (Bnd‘𝑌)) | 
| 79 | 77, 69, 78 | syl2anc 584 | . . . 4
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑑 ∈ ℝ ∧ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑))) → ((𝑀 ↾ ((𝑃(ball‘𝑀)𝑑) × (𝑃(ball‘𝑀)𝑑))) ↾ (𝑌 × 𝑌)) ∈ (Bnd‘𝑌)) | 
| 80 | 73, 79 | eqeltrrd 2841 | . . 3
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑑 ∈ ℝ ∧ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑))) → 𝑁 ∈ (Bnd‘𝑌)) | 
| 81 | 80 | rexlimdvaa 3155 | . 2
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) → (∃𝑑 ∈ ℝ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑) → 𝑁 ∈ (Bnd‘𝑌))) | 
| 82 | 68, 81 | impbid 212 | 1
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) → (𝑁 ∈ (Bnd‘𝑌) ↔ ∃𝑑 ∈ ℝ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑))) |