Step | Hyp | Ref
| Expression |
1 | | metres2 22970 |
. . . 4
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) → (𝑀 ↾ (𝑆 × 𝑆)) ∈ (Met‘𝑆)) |
2 | 1 | adantlr 714 |
. . 3
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ∀𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟)) ∧ 𝑆 ⊆ 𝑋) → (𝑀 ↾ (𝑆 × 𝑆)) ∈ (Met‘𝑆)) |
3 | | ssel2 3910 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ⊆ 𝑋 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑋) |
4 | 3 | ancoms 462 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝑆 ∧ 𝑆 ⊆ 𝑋) → 𝑥 ∈ 𝑋) |
5 | | oveq1 7142 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑥 → (𝑦(ball‘𝑀)𝑟) = (𝑥(ball‘𝑀)𝑟)) |
6 | 5 | eqeq2d 2809 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑥 → (𝑋 = (𝑦(ball‘𝑀)𝑟) ↔ 𝑋 = (𝑥(ball‘𝑀)𝑟))) |
7 | 6 | rexbidv 3256 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑥 → (∃𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟) ↔ ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑀)𝑟))) |
8 | 7 | rspcva 3569 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟)) → ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑀)𝑟)) |
9 | 4, 8 | sylan 583 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ 𝑆 ∧ 𝑆 ⊆ 𝑋) ∧ ∀𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟)) → ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑀)𝑟)) |
10 | 9 | adantlll 717 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ 𝑆) ∧ 𝑆 ⊆ 𝑋) ∧ ∀𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟)) → ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑀)𝑟)) |
11 | | dfss 3899 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑆 ⊆ 𝑋 ↔ 𝑆 = (𝑆 ∩ 𝑋)) |
12 | 11 | biimpi 219 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑆 ⊆ 𝑋 → 𝑆 = (𝑆 ∩ 𝑋)) |
13 | | incom 4128 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑆 ∩ 𝑋) = (𝑋 ∩ 𝑆) |
14 | 12, 13 | eqtrdi 2849 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑆 ⊆ 𝑋 → 𝑆 = (𝑋 ∩ 𝑆)) |
15 | | ineq1 4131 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑋 = (𝑥(ball‘𝑀)𝑟) → (𝑋 ∩ 𝑆) = ((𝑥(ball‘𝑀)𝑟) ∩ 𝑆)) |
16 | 14, 15 | sylan9eq 2853 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑆 ⊆ 𝑋 ∧ 𝑋 = (𝑥(ball‘𝑀)𝑟)) → 𝑆 = ((𝑥(ball‘𝑀)𝑟) ∩ 𝑆)) |
17 | 16 | adantll 713 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ 𝑆) ∧ 𝑆 ⊆ 𝑋) ∧ 𝑋 = (𝑥(ball‘𝑀)𝑟)) → 𝑆 = ((𝑥(ball‘𝑀)𝑟) ∩ 𝑆)) |
18 | 17 | adantlr 714 |
. . . . . . . . . . . . . 14
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑥 ∈ 𝑆) ∧ 𝑆 ⊆ 𝑋) ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑥(ball‘𝑀)𝑟)) → 𝑆 = ((𝑥(ball‘𝑀)𝑟) ∩ 𝑆)) |
19 | | eqid 2798 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑀 ↾ (𝑆 × 𝑆)) = (𝑀 ↾ (𝑆 × 𝑆)) |
20 | 19 | blssp 35194 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝑥 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+)) → (𝑥(ball‘(𝑀 ↾ (𝑆 × 𝑆)))𝑟) = ((𝑥(ball‘𝑀)𝑟) ∩ 𝑆)) |
21 | 20 | an4s 659 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ 𝑆) ∧ (𝑆 ⊆ 𝑋 ∧ 𝑟 ∈ ℝ+)) → (𝑥(ball‘(𝑀 ↾ (𝑆 × 𝑆)))𝑟) = ((𝑥(ball‘𝑀)𝑟) ∩ 𝑆)) |
22 | 21 | anassrs 471 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ 𝑆) ∧ 𝑆 ⊆ 𝑋) ∧ 𝑟 ∈ ℝ+) → (𝑥(ball‘(𝑀 ↾ (𝑆 × 𝑆)))𝑟) = ((𝑥(ball‘𝑀)𝑟) ∩ 𝑆)) |
23 | 22 | adantr 484 |
. . . . . . . . . . . . . 14
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑥 ∈ 𝑆) ∧ 𝑆 ⊆ 𝑋) ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑥(ball‘𝑀)𝑟)) → (𝑥(ball‘(𝑀 ↾ (𝑆 × 𝑆)))𝑟) = ((𝑥(ball‘𝑀)𝑟) ∩ 𝑆)) |
24 | 18, 23 | eqtr4d 2836 |
. . . . . . . . . . . . 13
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑥 ∈ 𝑆) ∧ 𝑆 ⊆ 𝑋) ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑥(ball‘𝑀)𝑟)) → 𝑆 = (𝑥(ball‘(𝑀 ↾ (𝑆 × 𝑆)))𝑟)) |
25 | 24 | ex 416 |
. . . . . . . . . . . 12
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ 𝑆) ∧ 𝑆 ⊆ 𝑋) ∧ 𝑟 ∈ ℝ+) → (𝑋 = (𝑥(ball‘𝑀)𝑟) → 𝑆 = (𝑥(ball‘(𝑀 ↾ (𝑆 × 𝑆)))𝑟))) |
26 | 25 | reximdva 3233 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ 𝑆) ∧ 𝑆 ⊆ 𝑋) → (∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑀)𝑟) → ∃𝑟 ∈ ℝ+ 𝑆 = (𝑥(ball‘(𝑀 ↾ (𝑆 × 𝑆)))𝑟))) |
27 | 26 | imp 410 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ 𝑆) ∧ 𝑆 ⊆ 𝑋) ∧ ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑀)𝑟)) → ∃𝑟 ∈ ℝ+ 𝑆 = (𝑥(ball‘(𝑀 ↾ (𝑆 × 𝑆)))𝑟)) |
28 | 10, 27 | syldan 594 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ 𝑆) ∧ 𝑆 ⊆ 𝑋) ∧ ∀𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟)) → ∃𝑟 ∈ ℝ+ 𝑆 = (𝑥(ball‘(𝑀 ↾ (𝑆 × 𝑆)))𝑟)) |
29 | 28 | an32s 651 |
. . . . . . . 8
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ 𝑆) ∧ ∀𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟)) ∧ 𝑆 ⊆ 𝑋) → ∃𝑟 ∈ ℝ+ 𝑆 = (𝑥(ball‘(𝑀 ↾ (𝑆 × 𝑆)))𝑟)) |
30 | 29 | ex 416 |
. . . . . . 7
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ 𝑆) ∧ ∀𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟)) → (𝑆 ⊆ 𝑋 → ∃𝑟 ∈ ℝ+ 𝑆 = (𝑥(ball‘(𝑀 ↾ (𝑆 × 𝑆)))𝑟))) |
31 | 30 | an32s 651 |
. . . . . 6
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ∀𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟)) ∧ 𝑥 ∈ 𝑆) → (𝑆 ⊆ 𝑋 → ∃𝑟 ∈ ℝ+ 𝑆 = (𝑥(ball‘(𝑀 ↾ (𝑆 × 𝑆)))𝑟))) |
32 | 31 | imp 410 |
. . . . 5
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ ∀𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟)) ∧ 𝑥 ∈ 𝑆) ∧ 𝑆 ⊆ 𝑋) → ∃𝑟 ∈ ℝ+ 𝑆 = (𝑥(ball‘(𝑀 ↾ (𝑆 × 𝑆)))𝑟)) |
33 | 32 | an32s 651 |
. . . 4
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ ∀𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟)) ∧ 𝑆 ⊆ 𝑋) ∧ 𝑥 ∈ 𝑆) → ∃𝑟 ∈ ℝ+ 𝑆 = (𝑥(ball‘(𝑀 ↾ (𝑆 × 𝑆)))𝑟)) |
34 | 33 | ralrimiva 3149 |
. . 3
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ∀𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟)) ∧ 𝑆 ⊆ 𝑋) → ∀𝑥 ∈ 𝑆 ∃𝑟 ∈ ℝ+ 𝑆 = (𝑥(ball‘(𝑀 ↾ (𝑆 × 𝑆)))𝑟)) |
35 | 2, 34 | jca 515 |
. 2
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ∀𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟)) ∧ 𝑆 ⊆ 𝑋) → ((𝑀 ↾ (𝑆 × 𝑆)) ∈ (Met‘𝑆) ∧ ∀𝑥 ∈ 𝑆 ∃𝑟 ∈ ℝ+ 𝑆 = (𝑥(ball‘(𝑀 ↾ (𝑆 × 𝑆)))𝑟))) |
36 | | isbnd 35218 |
. . 3
⊢ (𝑀 ∈ (Bnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∀𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟))) |
37 | 36 | anbi1i 626 |
. 2
⊢ ((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑆 ⊆ 𝑋) ↔ ((𝑀 ∈ (Met‘𝑋) ∧ ∀𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟)) ∧ 𝑆 ⊆ 𝑋)) |
38 | | isbnd 35218 |
. 2
⊢ ((𝑀 ↾ (𝑆 × 𝑆)) ∈ (Bnd‘𝑆) ↔ ((𝑀 ↾ (𝑆 × 𝑆)) ∈ (Met‘𝑆) ∧ ∀𝑥 ∈ 𝑆 ∃𝑟 ∈ ℝ+ 𝑆 = (𝑥(ball‘(𝑀 ↾ (𝑆 × 𝑆)))𝑟))) |
39 | 35, 37, 38 | 3imtr4i 295 |
1
⊢ ((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑆 ⊆ 𝑋) → (𝑀 ↾ (𝑆 × 𝑆)) ∈ (Bnd‘𝑆)) |