Metamath Proof Explorer

Theorem elbl2ps

Description: Membership in a ball. (Contributed by NM, 9-Mar-2007) (Revised by Thierry Arnoux, 11-Mar-2018)

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

Proof

Step Hyp Ref Expression
1 simprr 
 |-  ( ( ( D e. ( PsMet ` X ) /\ R e. RR* ) /\ ( P e. X /\ A e. X ) ) -> A e. X )
2 elblps 
 |-  ( ( D e. ( PsMet ` X ) /\ P e. X /\ R e. RR* ) -> ( A e. ( P ( ball ` D ) R ) <-> ( A e. X /\ ( P D A ) < R ) ) )
3 2 3expa 
 |-  ( ( ( D e. ( PsMet ` X ) /\ P e. X ) /\ R e. RR* ) -> ( A e. ( P ( ball ` D ) R ) <-> ( A e. X /\ ( P D A ) < R ) ) )
4 3 an32s 
 |-  ( ( ( D e. ( PsMet ` X ) /\ R e. RR* ) /\ P e. X ) -> ( A e. ( P ( ball ` D ) R ) <-> ( A e. X /\ ( P D A ) < R ) ) )
5 4 adantrr 
 |-  ( ( ( D e. ( PsMet ` X ) /\ R e. RR* ) /\ ( P e. X /\ A e. X ) ) -> ( A e. ( P ( ball ` D ) R ) <-> ( A e. X /\ ( P D A ) < R ) ) )
6 1 5 mpbirand 
 |-  ( ( ( D e. ( PsMet ` X ) /\ R e. RR* ) /\ ( P e. X /\ A e. X ) ) -> ( A e. ( P ( ball ` D ) R ) <-> ( P D A ) < R ) )