Theorem metuust

Description: The uniform structure generated by metric D is a uniform structure. (Contributed by Thierry Arnoux, 1-Dec-2017) (Revised by Thierry Arnoux, 11-Feb-2018)

	Ref	Expression
Assertion	metuust	|- ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( metUnif ` D ) e. ( UnifOn ` X ) )

Proof

Step	Hyp	Ref	Expression
1		metuval	|- ( D e. ( PsMet ` X ) -> ( metUnif ` D ) = ( ( X X. X ) filGen ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) ) )
2	1	adantl	|- ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( metUnif ` D ) = ( ( X X. X ) filGen ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) ) )
3		oveq2	|- ( a = b -> ( 0 [,) a ) = ( 0 [,) b ) )
4	3	imaeq2d	|- ( a = b -> ( `' D " ( 0 [,) a ) ) = ( `' D " ( 0 [,) b ) ) )
5	4	cbvmptv	|- ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) = ( b e. RR+ |-> ( `' D " ( 0 [,) b ) ) )
6	5	rneqi	|- ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) = ran ( b e. RR+ |-> ( `' D " ( 0 [,) b ) ) )
7	6	metust	|- ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( ( X X. X ) filGen ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) ) e. ( UnifOn ` X ) )
8	2 7	eqeltrd	|- ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( metUnif ` D ) e. ( UnifOn ` X ) )