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 
|- ( ( ( D e. ( PsMet ` X ) /\ R e. RR+ ) /\ ( A e. X /\ B e. X ) ) -> ( B e. ( A ( ball ` D ) R ) <-> B ( `' D " ( 0 [,) R ) ) A ) )

Proof

Step Hyp Ref Expression
1 rpxr 
 |-  ( R e. RR+ -> R e. RR* )
2 blcomps 
 |-  ( ( ( D e. ( PsMet ` X ) /\ R e. RR* ) /\ ( A e. X /\ B e. X ) ) -> ( B e. ( A ( ball ` D ) R ) <-> A e. ( B ( ball ` D ) R ) ) )
3 1 2 sylanl2 
 |-  ( ( ( D e. ( PsMet ` X ) /\ R e. RR+ ) /\ ( A e. X /\ B e. X ) ) -> ( B e. ( A ( ball ` D ) R ) <-> A e. ( B ( ball ` D ) R ) ) )
4 simpll 
 |-  ( ( ( D e. ( PsMet ` X ) /\ R e. RR+ ) /\ ( A e. X /\ B e. X ) ) -> D e. ( PsMet ` X ) )
5 simprr 
 |-  ( ( ( D e. ( PsMet ` X ) /\ R e. RR+ ) /\ ( A e. X /\ B e. X ) ) -> B e. X )
6 simplr 
 |-  ( ( ( D e. ( PsMet ` X ) /\ R e. RR+ ) /\ ( A e. X /\ B e. X ) ) -> R e. RR+ )
7 blval2 
 |-  ( ( D e. ( PsMet ` X ) /\ B e. X /\ R e. RR+ ) -> ( B ( ball ` D ) R ) = ( ( `' D " ( 0 [,) R ) ) " { B } ) )
8 7 eleq2d 
 |-  ( ( D e. ( PsMet ` X ) /\ B e. X /\ R e. RR+ ) -> ( A e. ( B ( ball ` D ) R ) <-> A e. ( ( `' D " ( 0 [,) R ) ) " { B } ) ) )
9 4 5 6 8 syl3anc 
 |-  ( ( ( D e. ( PsMet ` X ) /\ R e. RR+ ) /\ ( A e. X /\ B e. X ) ) -> ( A e. ( B ( ball ` D ) R ) <-> A e. ( ( `' D " ( 0 [,) R ) ) " { B } ) ) )
10 elimasng 
 |-  ( ( B e. X /\ A e. X ) -> ( A e. ( ( `' D " ( 0 [,) R ) ) " { B } ) <-> <. B , A >. e. ( `' D " ( 0 [,) R ) ) ) )
11 df-br 
 |-  ( B ( `' D " ( 0 [,) R ) ) A <-> <. B , A >. e. ( `' D " ( 0 [,) R ) ) )
12 10 11 bitr4di 
 |-  ( ( B e. X /\ A e. X ) -> ( A e. ( ( `' D " ( 0 [,) R ) ) " { B } ) <-> B ( `' D " ( 0 [,) R ) ) A ) )
13 12 ancoms 
 |-  ( ( A e. X /\ B e. X ) -> ( A e. ( ( `' D " ( 0 [,) R ) ) " { B } ) <-> B ( `' D " ( 0 [,) R ) ) A ) )
14 13 adantl 
 |-  ( ( ( D e. ( PsMet ` X ) /\ R e. RR+ ) /\ ( A e. X /\ B e. X ) ) -> ( A e. ( ( `' D " ( 0 [,) R ) ) " { B } ) <-> B ( `' D " ( 0 [,) R ) ) A ) )
15 3 9 14 3bitrd 
 |-  ( ( ( D e. ( PsMet ` X ) /\ R e. RR+ ) /\ ( A e. X /\ B e. X ) ) -> ( B e. ( A ( ball ` D ) R ) <-> B ( `' D " ( 0 [,) R ) ) A ) )