Metamath Proof Explorer

Theorem elbl3

Description: Membership in a ball, with reversed distance function arguments. (Contributed by NM, 10-Nov-2007)

Ref Expression
Assertion elbl3 
|- ( ( ( D e. ( *Met ` X ) /\ R e. RR* ) /\ ( P e. X /\ A e. X ) ) -> ( A e. ( P ( ball ` D ) R ) <-> ( A D P ) < R ) )

Proof

Step Hyp Ref Expression
1 elbl2 
 |-  ( ( ( D e. ( *Met ` X ) /\ R e. RR* ) /\ ( P e. X /\ A e. X ) ) -> ( A e. ( P ( ball ` D ) R ) <-> ( P D A ) < R ) )
2 xmetsym 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ A e. X ) -> ( P D A ) = ( A D P ) )
3 2 3expb 
 |-  ( ( D e. ( *Met ` X ) /\ ( P e. X /\ A e. X ) ) -> ( P D A ) = ( A D P ) )
4 3 adantlr 
 |-  ( ( ( D e. ( *Met ` X ) /\ R e. RR* ) /\ ( P e. X /\ A e. X ) ) -> ( P D A ) = ( A D P ) )
5 4 breq1d 
 |-  ( ( ( D e. ( *Met ` X ) /\ R e. RR* ) /\ ( P e. X /\ A e. X ) ) -> ( ( P D A ) < R <-> ( A D P ) < R ) )
6 1 5 bitrd 
 |-  ( ( ( D e. ( *Met ` X ) /\ R e. RR* ) /\ ( P e. X /\ A e. X ) ) -> ( A e. ( P ( ball ` D ) R ) <-> ( A D P ) < R ) )