Theorem psmetxrge0

Description: The distance function of a pseudometric space is a function into the nonnegative extended real numbers. (Contributed by Thierry Arnoux, 24-Feb-2018)

	Ref	Expression
Assertion	psmetxrge0	|- ( D e. ( PsMet ` X ) -> D : ( X X. X ) --> ( 0 [,] +oo ) )

Proof

Step	Hyp	Ref	Expression
1		psmetf	|- ( D e. ( PsMet ` X ) -> D : ( X X. X ) --> RR* )
2	1	ffnd	|- ( D e. ( PsMet ` X ) -> D Fn ( X X. X ) )
3	1	ffvelrnda	|- ( ( D e. ( PsMet ` X ) /\ a e. ( X X. X ) ) -> ( D ` a ) e. RR* )
4		elxp6	|- ( a e. ( X X. X ) <-> ( a = <. ( 1st ` a ) , ( 2nd ` a ) >. /\ ( ( 1st ` a ) e. X /\ ( 2nd ` a ) e. X ) ) )
5	4	simprbi	|- ( a e. ( X X. X ) -> ( ( 1st ` a ) e. X /\ ( 2nd ` a ) e. X ) )
6		psmetge0	|- ( ( D e. ( PsMet ` X ) /\ ( 1st ` a ) e. X /\ ( 2nd ` a ) e. X ) -> 0 <_ ( ( 1st ` a ) D ( 2nd ` a ) ) )
7	6	3expb	|- ( ( D e. ( PsMet ` X ) /\ ( ( 1st ` a ) e. X /\ ( 2nd ` a ) e. X ) ) -> 0 <_ ( ( 1st ` a ) D ( 2nd ` a ) ) )
8	5 7	sylan2	|- ( ( D e. ( PsMet ` X ) /\ a e. ( X X. X ) ) -> 0 <_ ( ( 1st ` a ) D ( 2nd ` a ) ) )
9		1st2nd2	|- ( a e. ( X X. X ) -> a = <. ( 1st ` a ) , ( 2nd ` a ) >. )
10	9	fveq2d	|- ( a e. ( X X. X ) -> ( D ` a ) = ( D ` <. ( 1st ` a ) , ( 2nd ` a ) >. ) )
11		df-ov	|- ( ( 1st ` a ) D ( 2nd ` a ) ) = ( D ` <. ( 1st ` a ) , ( 2nd ` a ) >. )
12	10 11	eqtr4di	|- ( a e. ( X X. X ) -> ( D ` a ) = ( ( 1st ` a ) D ( 2nd ` a ) ) )
13	12	adantl	|- ( ( D e. ( PsMet ` X ) /\ a e. ( X X. X ) ) -> ( D ` a ) = ( ( 1st ` a ) D ( 2nd ` a ) ) )
14	8 13	breqtrrd	|- ( ( D e. ( PsMet ` X ) /\ a e. ( X X. X ) ) -> 0 <_ ( D ` a ) )
15		elxrge0	|- ( ( D ` a ) e. ( 0 [,] +oo ) <-> ( ( D ` a ) e. RR* /\ 0 <_ ( D ` a ) ) )
16	3 14 15	sylanbrc	|- ( ( D e. ( PsMet ` X ) /\ a e. ( X X. X ) ) -> ( D ` a ) e. ( 0 [,] +oo ) )
17	16	ralrimiva	|- ( D e. ( PsMet ` X ) -> A. a e. ( X X. X ) ( D ` a ) e. ( 0 [,] +oo ) )
18		fnfvrnss	|- ( ( D Fn ( X X. X ) /\ A. a e. ( X X. X ) ( D ` a ) e. ( 0 [,] +oo ) ) -> ran D C_ ( 0 [,] +oo ) )
19	2 17 18	syl2anc	|- ( D e. ( PsMet ` X ) -> ran D C_ ( 0 [,] +oo ) )
20		df-f	|- ( D : ( X X. X ) --> ( 0 [,] +oo ) <-> ( D Fn ( X X. X ) /\ ran D C_ ( 0 [,] +oo ) ) )
21	2 19 20	sylanbrc	|- ( D e. ( PsMet ` X ) -> D : ( X X. X ) --> ( 0 [,] +oo ) )