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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | psmetf | |
|
2 | 1 | ffnd | |
3 | 1 | ffvelrnda | |
4 | elxp6 | |
|
5 | 4 | simprbi | |
6 | psmetge0 | |
|
7 | 6 | 3expb | |
8 | 5 7 | sylan2 | |
9 | 1st2nd2 | |
|
10 | 9 | fveq2d | |
11 | df-ov | |
|
12 | 10 11 | eqtr4di | |
13 | 12 | adantl | |
14 | 8 13 | breqtrrd | |
15 | elxrge0 | |
|
16 | 3 14 15 | sylanbrc | |
17 | 16 | ralrimiva | |
18 | fnfvrnss | |
|
19 | 2 17 18 | syl2anc | |
20 | df-f | |
|
21 | 2 19 20 | sylanbrc | |