Step |
Hyp |
Ref |
Expression |
1 |
|
simp2 |
⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ ( 𝑅 ∈ ℝ* ∧ 0 < 𝑅 ) ) → 𝑃 ∈ 𝑋 ) |
2 |
|
psmet0 |
⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝑃 𝐷 𝑃 ) = 0 ) |
3 |
2
|
3adant3 |
⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ ( 𝑅 ∈ ℝ* ∧ 0 < 𝑅 ) ) → ( 𝑃 𝐷 𝑃 ) = 0 ) |
4 |
|
simp3r |
⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ ( 𝑅 ∈ ℝ* ∧ 0 < 𝑅 ) ) → 0 < 𝑅 ) |
5 |
3 4
|
eqbrtrd |
⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ ( 𝑅 ∈ ℝ* ∧ 0 < 𝑅 ) ) → ( 𝑃 𝐷 𝑃 ) < 𝑅 ) |
6 |
|
elblps |
⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → ( 𝑃 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ↔ ( 𝑃 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑃 ) < 𝑅 ) ) ) |
7 |
6
|
3adant3r |
⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ ( 𝑅 ∈ ℝ* ∧ 0 < 𝑅 ) ) → ( 𝑃 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ↔ ( 𝑃 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑃 ) < 𝑅 ) ) ) |
8 |
1 5 7
|
mpbir2and |
⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ ( 𝑅 ∈ ℝ* ∧ 0 < 𝑅 ) ) → 𝑃 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) |