Metamath Proof Explorer


Theorem elbl4

Description: Membership in a ball, alternative definition. (Contributed by Thierry Arnoux, 26-Jan-2018) (Revised by Thierry Arnoux, 11-Mar-2018)

Ref Expression
Assertion elbl4 ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝐴𝑋𝐵𝑋 ) ) → ( 𝐵 ∈ ( 𝐴 ( ball ‘ 𝐷 ) 𝑅 ) ↔ 𝐵 ( 𝐷 “ ( 0 [,) 𝑅 ) ) 𝐴 ) )

Proof

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 [,) 𝑅 ) ) 𝐴 ) )