Step | Hyp | Ref
| Expression |
1 | | elinel2 3322 |
. . . . . . . . 9
⊢ (𝑃 ∈ (𝑋 ∩ 𝑌) → 𝑃 ∈ 𝑌) |
2 | | blres.2 |
. . . . . . . . . . 11
⊢ 𝐶 = (𝐷 ↾ (𝑌 × 𝑌)) |
3 | 2 | oveqi 5882 |
. . . . . . . . . 10
⊢ (𝑃𝐶𝑥) = (𝑃(𝐷 ↾ (𝑌 × 𝑌))𝑥) |
4 | | ovres 6008 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ 𝑌 ∧ 𝑥 ∈ 𝑌) → (𝑃(𝐷 ↾ (𝑌 × 𝑌))𝑥) = (𝑃𝐷𝑥)) |
5 | 3, 4 | eqtrid 2222 |
. . . . . . . . 9
⊢ ((𝑃 ∈ 𝑌 ∧ 𝑥 ∈ 𝑌) → (𝑃𝐶𝑥) = (𝑃𝐷𝑥)) |
6 | 1, 5 | sylan 283 |
. . . . . . . 8
⊢ ((𝑃 ∈ (𝑋 ∩ 𝑌) ∧ 𝑥 ∈ 𝑌) → (𝑃𝐶𝑥) = (𝑃𝐷𝑥)) |
7 | 6 | breq1d 4010 |
. . . . . . 7
⊢ ((𝑃 ∈ (𝑋 ∩ 𝑌) ∧ 𝑥 ∈ 𝑌) → ((𝑃𝐶𝑥) < 𝑅 ↔ (𝑃𝐷𝑥) < 𝑅)) |
8 | 7 | anbi2d 464 |
. . . . . 6
⊢ ((𝑃 ∈ (𝑋 ∩ 𝑌) ∧ 𝑥 ∈ 𝑌) → ((𝑥 ∈ 𝑋 ∧ (𝑃𝐶𝑥) < 𝑅) ↔ (𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < 𝑅))) |
9 | 8 | pm5.32da 452 |
. . . . 5
⊢ (𝑃 ∈ (𝑋 ∩ 𝑌) → ((𝑥 ∈ 𝑌 ∧ (𝑥 ∈ 𝑋 ∧ (𝑃𝐶𝑥) < 𝑅)) ↔ (𝑥 ∈ 𝑌 ∧ (𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < 𝑅)))) |
10 | 9 | 3ad2ant2 1019 |
. . . 4
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ (𝑋 ∩ 𝑌) ∧ 𝑅 ∈ ℝ*) → ((𝑥 ∈ 𝑌 ∧ (𝑥 ∈ 𝑋 ∧ (𝑃𝐶𝑥) < 𝑅)) ↔ (𝑥 ∈ 𝑌 ∧ (𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < 𝑅)))) |
11 | | elin 3318 |
. . . . . . 7
⊢ (𝑥 ∈ (𝑋 ∩ 𝑌) ↔ (𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑌)) |
12 | | ancom 266 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑌) ↔ (𝑥 ∈ 𝑌 ∧ 𝑥 ∈ 𝑋)) |
13 | 11, 12 | bitri 184 |
. . . . . 6
⊢ (𝑥 ∈ (𝑋 ∩ 𝑌) ↔ (𝑥 ∈ 𝑌 ∧ 𝑥 ∈ 𝑋)) |
14 | 13 | anbi1i 458 |
. . . . 5
⊢ ((𝑥 ∈ (𝑋 ∩ 𝑌) ∧ (𝑃𝐶𝑥) < 𝑅) ↔ ((𝑥 ∈ 𝑌 ∧ 𝑥 ∈ 𝑋) ∧ (𝑃𝐶𝑥) < 𝑅)) |
15 | | anass 401 |
. . . . 5
⊢ (((𝑥 ∈ 𝑌 ∧ 𝑥 ∈ 𝑋) ∧ (𝑃𝐶𝑥) < 𝑅) ↔ (𝑥 ∈ 𝑌 ∧ (𝑥 ∈ 𝑋 ∧ (𝑃𝐶𝑥) < 𝑅))) |
16 | 14, 15 | bitri 184 |
. . . 4
⊢ ((𝑥 ∈ (𝑋 ∩ 𝑌) ∧ (𝑃𝐶𝑥) < 𝑅) ↔ (𝑥 ∈ 𝑌 ∧ (𝑥 ∈ 𝑋 ∧ (𝑃𝐶𝑥) < 𝑅))) |
17 | | ancom 266 |
. . . 4
⊢ (((𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < 𝑅) ∧ 𝑥 ∈ 𝑌) ↔ (𝑥 ∈ 𝑌 ∧ (𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < 𝑅))) |
18 | 10, 16, 17 | 3bitr4g 223 |
. . 3
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ (𝑋 ∩ 𝑌) ∧ 𝑅 ∈ ℝ*) → ((𝑥 ∈ (𝑋 ∩ 𝑌) ∧ (𝑃𝐶𝑥) < 𝑅) ↔ ((𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < 𝑅) ∧ 𝑥 ∈ 𝑌))) |
19 | | xmetres 13549 |
. . . . 5
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐷 ↾ (𝑌 × 𝑌)) ∈ (∞Met‘(𝑋 ∩ 𝑌))) |
20 | 2, 19 | eqeltrid 2264 |
. . . 4
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐶 ∈ (∞Met‘(𝑋 ∩ 𝑌))) |
21 | | elbl 13558 |
. . . 4
⊢ ((𝐶 ∈ (∞Met‘(𝑋 ∩ 𝑌)) ∧ 𝑃 ∈ (𝑋 ∩ 𝑌) ∧ 𝑅 ∈ ℝ*) → (𝑥 ∈ (𝑃(ball‘𝐶)𝑅) ↔ (𝑥 ∈ (𝑋 ∩ 𝑌) ∧ (𝑃𝐶𝑥) < 𝑅))) |
22 | 20, 21 | syl3an1 1271 |
. . 3
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ (𝑋 ∩ 𝑌) ∧ 𝑅 ∈ ℝ*) → (𝑥 ∈ (𝑃(ball‘𝐶)𝑅) ↔ (𝑥 ∈ (𝑋 ∩ 𝑌) ∧ (𝑃𝐶𝑥) < 𝑅))) |
23 | | elin 3318 |
. . . 4
⊢ (𝑥 ∈ ((𝑃(ball‘𝐷)𝑅) ∩ 𝑌) ↔ (𝑥 ∈ (𝑃(ball‘𝐷)𝑅) ∧ 𝑥 ∈ 𝑌)) |
24 | | elinel1 3321 |
. . . . . 6
⊢ (𝑃 ∈ (𝑋 ∩ 𝑌) → 𝑃 ∈ 𝑋) |
25 | | elbl 13558 |
. . . . . 6
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝑥 ∈ (𝑃(ball‘𝐷)𝑅) ↔ (𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < 𝑅))) |
26 | 24, 25 | syl3an2 1272 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ (𝑋 ∩ 𝑌) ∧ 𝑅 ∈ ℝ*) → (𝑥 ∈ (𝑃(ball‘𝐷)𝑅) ↔ (𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < 𝑅))) |
27 | 26 | anbi1d 465 |
. . . 4
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ (𝑋 ∩ 𝑌) ∧ 𝑅 ∈ ℝ*) → ((𝑥 ∈ (𝑃(ball‘𝐷)𝑅) ∧ 𝑥 ∈ 𝑌) ↔ ((𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < 𝑅) ∧ 𝑥 ∈ 𝑌))) |
28 | 23, 27 | bitrid 192 |
. . 3
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ (𝑋 ∩ 𝑌) ∧ 𝑅 ∈ ℝ*) → (𝑥 ∈ ((𝑃(ball‘𝐷)𝑅) ∩ 𝑌) ↔ ((𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < 𝑅) ∧ 𝑥 ∈ 𝑌))) |
29 | 18, 22, 28 | 3bitr4d 220 |
. 2
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ (𝑋 ∩ 𝑌) ∧ 𝑅 ∈ ℝ*) → (𝑥 ∈ (𝑃(ball‘𝐶)𝑅) ↔ 𝑥 ∈ ((𝑃(ball‘𝐷)𝑅) ∩ 𝑌))) |
30 | 29 | eqrdv 2175 |
1
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ (𝑋 ∩ 𝑌) ∧ 𝑅 ∈ ℝ*) → (𝑃(ball‘𝐶)𝑅) = ((𝑃(ball‘𝐷)𝑅) ∩ 𝑌)) |