Metamath Proof Explorer

Theorem blfval

Description: The value of the ball function. (Contributed by NM, 30-Aug-2006) (Revised by Mario Carneiro, 11-Nov-2013) (Proof shortened by Thierry Arnoux, 11-Feb-2018)

		Ref	Expression
	Assertion	blfval	\|- ( D e. ( Met ` X ) -> ( ball ` D ) = ( x e. X , r e. RR \|-> { y e. X \| ( x D y ) < r } ) )

Proof

Step	Hyp	Ref	Expression
1		xmetpsmet	\|- ( D e. ( *Met ` X ) -> D e. ( PsMet ` X ) )
2		blfvalps	\|- ( D e. ( PsMet ` X ) -> ( ball ` D ) = ( x e. X , r e. RR* \|-> { y e. X \| ( x D y ) < r } ) )
3	1 2	syl	\|- ( D e. ( Met ` X ) -> ( ball ` D ) = ( x e. X , r e. RR \|-> { y e. X \| ( x D y ) < r } ) )

Step

Hyp

Ref

Expression

xmetpsmet

 |-  ( D e. ( *Met ` X ) -> D e. ( PsMet ` X ) )

blfvalps

 |-  ( D e. ( PsMet ` X ) -> ( ball ` D ) = ( x e. X , r e. RR* |-> { y e. X | ( x D y ) < r } ) )

1 2

syl

 |-  ( D e. ( *Met ` X ) -> ( ball ` D ) = ( x e. X , r e. RR* |-> { y e. X | ( x D y ) < r } ) )