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 DPsMetXD:X×X0+∞

Proof

Step Hyp Ref Expression
1 psmetf DPsMetXD:X×X*
2 1 ffnd DPsMetXDFnX×X
3 1 ffvelrnda DPsMetXaX×XDa*
4 elxp6 aX×Xa=1sta2nda1staX2ndaX
5 4 simprbi aX×X1staX2ndaX
6 psmetge0 DPsMetX1staX2ndaX01staD2nda
7 6 3expb DPsMetX1staX2ndaX01staD2nda
8 5 7 sylan2 DPsMetXaX×X01staD2nda
9 1st2nd2 aX×Xa=1sta2nda
10 9 fveq2d aX×XDa=D1sta2nda
11 df-ov 1staD2nda=D1sta2nda
12 10 11 eqtr4di aX×XDa=1staD2nda
13 12 adantl DPsMetXaX×XDa=1staD2nda
14 8 13 breqtrrd DPsMetXaX×X0Da
15 elxrge0 Da0+∞Da*0Da
16 3 14 15 sylanbrc DPsMetXaX×XDa0+∞
17 16 ralrimiva DPsMetXaX×XDa0+∞
18 fnfvrnss DFnX×XaX×XDa0+∞ranD0+∞
19 2 17 18 syl2anc DPsMetXranD0+∞
20 df-f D:X×X0+∞DFnX×XranD0+∞
21 2 19 20 sylanbrc DPsMetXD:X×X0+∞