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

Metamath Proof Explorer

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