Step |
Hyp |
Ref |
Expression |
1 |
|
rpxr |
⊢ ( 𝑅 ∈ ℝ+ → 𝑅 ∈ ℝ* ) |
2 |
|
blcomps |
⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ* ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐵 ∈ ( 𝐴 ( ball ‘ 𝐷 ) 𝑅 ) ↔ 𝐴 ∈ ( 𝐵 ( ball ‘ 𝐷 ) 𝑅 ) ) ) |
3 |
1 2
|
sylanl2 |
⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐵 ∈ ( 𝐴 ( ball ‘ 𝐷 ) 𝑅 ) ↔ 𝐴 ∈ ( 𝐵 ( ball ‘ 𝐷 ) 𝑅 ) ) ) |
4 |
|
simpll |
⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) |
5 |
|
simprr |
⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → 𝐵 ∈ 𝑋 ) |
6 |
|
simplr |
⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → 𝑅 ∈ ℝ+ ) |
7 |
|
blval2 |
⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐵 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+ ) → ( 𝐵 ( ball ‘ 𝐷 ) 𝑅 ) = ( ( ◡ 𝐷 “ ( 0 [,) 𝑅 ) ) “ { 𝐵 } ) ) |
8 |
7
|
eleq2d |
⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐵 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+ ) → ( 𝐴 ∈ ( 𝐵 ( ball ‘ 𝐷 ) 𝑅 ) ↔ 𝐴 ∈ ( ( ◡ 𝐷 “ ( 0 [,) 𝑅 ) ) “ { 𝐵 } ) ) ) |
9 |
4 5 6 8
|
syl3anc |
⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 ∈ ( 𝐵 ( ball ‘ 𝐷 ) 𝑅 ) ↔ 𝐴 ∈ ( ( ◡ 𝐷 “ ( 0 [,) 𝑅 ) ) “ { 𝐵 } ) ) ) |
10 |
|
elimasng |
⊢ ( ( 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ∈ ( ( ◡ 𝐷 “ ( 0 [,) 𝑅 ) ) “ { 𝐵 } ) ↔ 〈 𝐵 , 𝐴 〉 ∈ ( ◡ 𝐷 “ ( 0 [,) 𝑅 ) ) ) ) |
11 |
|
df-br |
⊢ ( 𝐵 ( ◡ 𝐷 “ ( 0 [,) 𝑅 ) ) 𝐴 ↔ 〈 𝐵 , 𝐴 〉 ∈ ( ◡ 𝐷 “ ( 0 [,) 𝑅 ) ) ) |
12 |
10 11
|
bitr4di |
⊢ ( ( 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ∈ ( ( ◡ 𝐷 “ ( 0 [,) 𝑅 ) ) “ { 𝐵 } ) ↔ 𝐵 ( ◡ 𝐷 “ ( 0 [,) 𝑅 ) ) 𝐴 ) ) |
13 |
12
|
ancoms |
⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ∈ ( ( ◡ 𝐷 “ ( 0 [,) 𝑅 ) ) “ { 𝐵 } ) ↔ 𝐵 ( ◡ 𝐷 “ ( 0 [,) 𝑅 ) ) 𝐴 ) ) |
14 |
13
|
adantl |
⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 ∈ ( ( ◡ 𝐷 “ ( 0 [,) 𝑅 ) ) “ { 𝐵 } ) ↔ 𝐵 ( ◡ 𝐷 “ ( 0 [,) 𝑅 ) ) 𝐴 ) ) |
15 |
3 9 14
|
3bitrd |
⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐵 ∈ ( 𝐴 ( ball ‘ 𝐷 ) 𝑅 ) ↔ 𝐵 ( ◡ 𝐷 “ ( 0 [,) 𝑅 ) ) 𝐴 ) ) |