Step | Hyp | Ref
| Expression |
1 | | elinel2 4086 |
. . . . . . . . 9
⊢ (𝑃 ∈ (𝑋 ∩ 𝑌) → 𝑃 ∈ 𝑌) |
2 | | blres.2 |
. . . . . . . . . . 11
⊢ 𝐶 = (𝐷 ↾ (𝑌 × 𝑌)) |
3 | 2 | oveqi 7183 |
. . . . . . . . . 10
⊢ (𝑃𝐶𝑥) = (𝑃(𝐷 ↾ (𝑌 × 𝑌))𝑥) |
4 | | ovres 7330 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ 𝑌 ∧ 𝑥 ∈ 𝑌) → (𝑃(𝐷 ↾ (𝑌 × 𝑌))𝑥) = (𝑃𝐷𝑥)) |
5 | 3, 4 | syl5eq 2785 |
. . . . . . . . 9
⊢ ((𝑃 ∈ 𝑌 ∧ 𝑥 ∈ 𝑌) → (𝑃𝐶𝑥) = (𝑃𝐷𝑥)) |
6 | 1, 5 | sylan 583 |
. . . . . . . 8
⊢ ((𝑃 ∈ (𝑋 ∩ 𝑌) ∧ 𝑥 ∈ 𝑌) → (𝑃𝐶𝑥) = (𝑃𝐷𝑥)) |
7 | 6 | breq1d 5040 |
. . . . . . 7
⊢ ((𝑃 ∈ (𝑋 ∩ 𝑌) ∧ 𝑥 ∈ 𝑌) → ((𝑃𝐶𝑥) < 𝑅 ↔ (𝑃𝐷𝑥) < 𝑅)) |
8 | 7 | anbi2d 632 |
. . . . . 6
⊢ ((𝑃 ∈ (𝑋 ∩ 𝑌) ∧ 𝑥 ∈ 𝑌) → ((𝑥 ∈ 𝑋 ∧ (𝑃𝐶𝑥) < 𝑅) ↔ (𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < 𝑅))) |
9 | 8 | pm5.32da 582 |
. . . . 5
⊢ (𝑃 ∈ (𝑋 ∩ 𝑌) → ((𝑥 ∈ 𝑌 ∧ (𝑥 ∈ 𝑋 ∧ (𝑃𝐶𝑥) < 𝑅)) ↔ (𝑥 ∈ 𝑌 ∧ (𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < 𝑅)))) |
10 | 9 | 3ad2ant2 1135 |
. . . 4
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ (𝑋 ∩ 𝑌) ∧ 𝑅 ∈ ℝ*) → ((𝑥 ∈ 𝑌 ∧ (𝑥 ∈ 𝑋 ∧ (𝑃𝐶𝑥) < 𝑅)) ↔ (𝑥 ∈ 𝑌 ∧ (𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < 𝑅)))) |
11 | | elin 3859 |
. . . . . . 7
⊢ (𝑥 ∈ (𝑋 ∩ 𝑌) ↔ (𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑌)) |
12 | 11 | biancomi 466 |
. . . . . 6
⊢ (𝑥 ∈ (𝑋 ∩ 𝑌) ↔ (𝑥 ∈ 𝑌 ∧ 𝑥 ∈ 𝑋)) |
13 | 12 | anbi1i 627 |
. . . . 5
⊢ ((𝑥 ∈ (𝑋 ∩ 𝑌) ∧ (𝑃𝐶𝑥) < 𝑅) ↔ ((𝑥 ∈ 𝑌 ∧ 𝑥 ∈ 𝑋) ∧ (𝑃𝐶𝑥) < 𝑅)) |
14 | | anass 472 |
. . . . 5
⊢ (((𝑥 ∈ 𝑌 ∧ 𝑥 ∈ 𝑋) ∧ (𝑃𝐶𝑥) < 𝑅) ↔ (𝑥 ∈ 𝑌 ∧ (𝑥 ∈ 𝑋 ∧ (𝑃𝐶𝑥) < 𝑅))) |
15 | 13, 14 | bitri 278 |
. . . 4
⊢ ((𝑥 ∈ (𝑋 ∩ 𝑌) ∧ (𝑃𝐶𝑥) < 𝑅) ↔ (𝑥 ∈ 𝑌 ∧ (𝑥 ∈ 𝑋 ∧ (𝑃𝐶𝑥) < 𝑅))) |
16 | | ancom 464 |
. . . 4
⊢ (((𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < 𝑅) ∧ 𝑥 ∈ 𝑌) ↔ (𝑥 ∈ 𝑌 ∧ (𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < 𝑅))) |
17 | 10, 15, 16 | 3bitr4g 317 |
. . 3
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ (𝑋 ∩ 𝑌) ∧ 𝑅 ∈ ℝ*) → ((𝑥 ∈ (𝑋 ∩ 𝑌) ∧ (𝑃𝐶𝑥) < 𝑅) ↔ ((𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < 𝑅) ∧ 𝑥 ∈ 𝑌))) |
18 | | xmetres 23117 |
. . . . 5
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐷 ↾ (𝑌 × 𝑌)) ∈ (∞Met‘(𝑋 ∩ 𝑌))) |
19 | 2, 18 | eqeltrid 2837 |
. . . 4
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐶 ∈ (∞Met‘(𝑋 ∩ 𝑌))) |
20 | | elbl 23141 |
. . . 4
⊢ ((𝐶 ∈ (∞Met‘(𝑋 ∩ 𝑌)) ∧ 𝑃 ∈ (𝑋 ∩ 𝑌) ∧ 𝑅 ∈ ℝ*) → (𝑥 ∈ (𝑃(ball‘𝐶)𝑅) ↔ (𝑥 ∈ (𝑋 ∩ 𝑌) ∧ (𝑃𝐶𝑥) < 𝑅))) |
21 | 19, 20 | syl3an1 1164 |
. . 3
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ (𝑋 ∩ 𝑌) ∧ 𝑅 ∈ ℝ*) → (𝑥 ∈ (𝑃(ball‘𝐶)𝑅) ↔ (𝑥 ∈ (𝑋 ∩ 𝑌) ∧ (𝑃𝐶𝑥) < 𝑅))) |
22 | | elin 3859 |
. . . 4
⊢ (𝑥 ∈ ((𝑃(ball‘𝐷)𝑅) ∩ 𝑌) ↔ (𝑥 ∈ (𝑃(ball‘𝐷)𝑅) ∧ 𝑥 ∈ 𝑌)) |
23 | | elinel1 4085 |
. . . . . 6
⊢ (𝑃 ∈ (𝑋 ∩ 𝑌) → 𝑃 ∈ 𝑋) |
24 | | elbl 23141 |
. . . . . 6
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝑥 ∈ (𝑃(ball‘𝐷)𝑅) ↔ (𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < 𝑅))) |
25 | 23, 24 | syl3an2 1165 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ (𝑋 ∩ 𝑌) ∧ 𝑅 ∈ ℝ*) → (𝑥 ∈ (𝑃(ball‘𝐷)𝑅) ↔ (𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < 𝑅))) |
26 | 25 | anbi1d 633 |
. . . 4
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ (𝑋 ∩ 𝑌) ∧ 𝑅 ∈ ℝ*) → ((𝑥 ∈ (𝑃(ball‘𝐷)𝑅) ∧ 𝑥 ∈ 𝑌) ↔ ((𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < 𝑅) ∧ 𝑥 ∈ 𝑌))) |
27 | 22, 26 | syl5bb 286 |
. . 3
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ (𝑋 ∩ 𝑌) ∧ 𝑅 ∈ ℝ*) → (𝑥 ∈ ((𝑃(ball‘𝐷)𝑅) ∩ 𝑌) ↔ ((𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < 𝑅) ∧ 𝑥 ∈ 𝑌))) |
28 | 17, 21, 27 | 3bitr4d 314 |
. 2
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ (𝑋 ∩ 𝑌) ∧ 𝑅 ∈ ℝ*) → (𝑥 ∈ (𝑃(ball‘𝐶)𝑅) ↔ 𝑥 ∈ ((𝑃(ball‘𝐷)𝑅) ∩ 𝑌))) |
29 | 28 | eqrdv 2736 |
1
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ (𝑋 ∩ 𝑌) ∧ 𝑅 ∈ ℝ*) → (𝑃(ball‘𝐶)𝑅) = ((𝑃(ball‘𝐷)𝑅) ∩ 𝑌)) |