| Step |
Hyp |
Ref |
Expression |
| 1 |
|
blss |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝑃 ∈ 𝑥 ) → ∃ 𝑟 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑥 ) |
| 2 |
|
sstr |
⊢ ( ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐴 ) |
| 3 |
2
|
expcom |
⊢ ( 𝑥 ⊆ 𝐴 → ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑥 → ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐴 ) ) |
| 4 |
3
|
reximdv |
⊢ ( 𝑥 ⊆ 𝐴 → ( ∃ 𝑟 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑥 → ∃ 𝑟 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐴 ) ) |
| 5 |
1 4
|
syl5com |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝑃 ∈ 𝑥 ) → ( 𝑥 ⊆ 𝐴 → ∃ 𝑟 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐴 ) ) |
| 6 |
5
|
3expa |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ ran ( ball ‘ 𝐷 ) ) ∧ 𝑃 ∈ 𝑥 ) → ( 𝑥 ⊆ 𝐴 → ∃ 𝑟 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐴 ) ) |
| 7 |
6
|
expimpd |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ ran ( ball ‘ 𝐷 ) ) → ( ( 𝑃 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) → ∃ 𝑟 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐴 ) ) |
| 8 |
7
|
adantlr |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑥 ∈ ran ( ball ‘ 𝐷 ) ) → ( ( 𝑃 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) → ∃ 𝑟 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐴 ) ) |
| 9 |
8
|
rexlimdva |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( ∃ 𝑥 ∈ ran ( ball ‘ 𝐷 ) ( 𝑃 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) → ∃ 𝑟 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐴 ) ) |
| 10 |
|
simpll |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐴 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) |
| 11 |
|
simplr |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐴 ) ) → 𝑃 ∈ 𝑋 ) |
| 12 |
|
rpxr |
⊢ ( 𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ* ) |
| 13 |
12
|
ad2antrl |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐴 ) ) → 𝑟 ∈ ℝ* ) |
| 14 |
|
blelrn |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ∈ ran ( ball ‘ 𝐷 ) ) |
| 15 |
10 11 13 14
|
syl3anc |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐴 ) ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ∈ ran ( ball ‘ 𝐷 ) ) |
| 16 |
|
simprl |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐴 ) ) → 𝑟 ∈ ℝ+ ) |
| 17 |
|
blcntr |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) → 𝑃 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ) |
| 18 |
10 11 16 17
|
syl3anc |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐴 ) ) → 𝑃 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ) |
| 19 |
|
simprr |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐴 ) ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐴 ) |
| 20 |
|
eleq2 |
⊢ ( 𝑥 = ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) → ( 𝑃 ∈ 𝑥 ↔ 𝑃 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ) ) |
| 21 |
|
sseq1 |
⊢ ( 𝑥 = ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) → ( 𝑥 ⊆ 𝐴 ↔ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐴 ) ) |
| 22 |
20 21
|
anbi12d |
⊢ ( 𝑥 = ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) → ( ( 𝑃 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) ↔ ( 𝑃 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ∧ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐴 ) ) ) |
| 23 |
22
|
rspcev |
⊢ ( ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ∈ ran ( ball ‘ 𝐷 ) ∧ ( 𝑃 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ∧ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐴 ) ) → ∃ 𝑥 ∈ ran ( ball ‘ 𝐷 ) ( 𝑃 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) ) |
| 24 |
15 18 19 23
|
syl12anc |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐴 ) ) → ∃ 𝑥 ∈ ran ( ball ‘ 𝐷 ) ( 𝑃 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) ) |
| 25 |
24
|
rexlimdvaa |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( ∃ 𝑟 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐴 → ∃ 𝑥 ∈ ran ( ball ‘ 𝐷 ) ( 𝑃 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) ) ) |
| 26 |
9 25
|
impbid |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( ∃ 𝑥 ∈ ran ( ball ‘ 𝐷 ) ( 𝑃 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) ↔ ∃ 𝑟 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐴 ) ) |