This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )