Step |
Hyp |
Ref |
Expression |
1 |
|
mopni.1 |
⊢ 𝐽 = ( MetOpen ‘ 𝐷 ) |
2 |
|
blcld.3 |
⊢ 𝑆 = { 𝑧 ∈ 𝑋 ∣ ( 𝑃 𝐷 𝑧 ) ≤ 𝑅 } |
3 |
1 2
|
blcld |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) |
4 |
|
blssm |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ⊆ 𝑋 ) |
5 |
|
elbl |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → ( 𝑧 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ↔ ( 𝑧 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑧 ) < 𝑅 ) ) ) |
6 |
|
xmetcl |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) → ( 𝑃 𝐷 𝑧 ) ∈ ℝ* ) |
7 |
6
|
3expa |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑃 𝐷 𝑧 ) ∈ ℝ* ) |
8 |
7
|
3adantl3 |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑃 𝐷 𝑧 ) ∈ ℝ* ) |
9 |
|
simpl3 |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑧 ∈ 𝑋 ) → 𝑅 ∈ ℝ* ) |
10 |
|
xrltle |
⊢ ( ( ( 𝑃 𝐷 𝑧 ) ∈ ℝ* ∧ 𝑅 ∈ ℝ* ) → ( ( 𝑃 𝐷 𝑧 ) < 𝑅 → ( 𝑃 𝐷 𝑧 ) ≤ 𝑅 ) ) |
11 |
8 9 10
|
syl2anc |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝑃 𝐷 𝑧 ) < 𝑅 → ( 𝑃 𝐷 𝑧 ) ≤ 𝑅 ) ) |
12 |
11
|
expimpd |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → ( ( 𝑧 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑧 ) < 𝑅 ) → ( 𝑃 𝐷 𝑧 ) ≤ 𝑅 ) ) |
13 |
5 12
|
sylbid |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → ( 𝑧 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) → ( 𝑃 𝐷 𝑧 ) ≤ 𝑅 ) ) |
14 |
13
|
ralrimiv |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → ∀ 𝑧 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ( 𝑃 𝐷 𝑧 ) ≤ 𝑅 ) |
15 |
|
ssrab |
⊢ ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ⊆ { 𝑧 ∈ 𝑋 ∣ ( 𝑃 𝐷 𝑧 ) ≤ 𝑅 } ↔ ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ⊆ 𝑋 ∧ ∀ 𝑧 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ( 𝑃 𝐷 𝑧 ) ≤ 𝑅 ) ) |
16 |
4 14 15
|
sylanbrc |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ⊆ { 𝑧 ∈ 𝑋 ∣ ( 𝑃 𝐷 𝑧 ) ≤ 𝑅 } ) |
17 |
16 2
|
sseqtrrdi |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ⊆ 𝑆 ) |
18 |
|
eqid |
⊢ ∪ 𝐽 = ∪ 𝐽 |
19 |
18
|
clsss2 |
⊢ ( ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ⊆ 𝑆 ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ⊆ 𝑆 ) |
20 |
3 17 19
|
syl2anc |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ⊆ 𝑆 ) |