Metamath Proof Explorer


Theorem metdsf

Description: The distance from a point to a set is a nonnegative extended real number. (Contributed by Mario Carneiro, 14-Feb-2015) (Revised by Mario Carneiro, 4-Sep-2015) (Proof shortened by AV, 30-Sep-2020)

Ref Expression
Hypothesis metdscn.f F=xXsupranySxDy*<
Assertion metdsf D∞MetXSXF:X0+∞

Proof

Step Hyp Ref Expression
1 metdscn.f F=xXsupranySxDy*<
2 simplll D∞MetXSXxXySD∞MetX
3 simplr D∞MetXSXxXySxX
4 simplr D∞MetXSXxXSX
5 4 sselda D∞MetXSXxXySyX
6 xmetcl D∞MetXxXyXxDy*
7 2 3 5 6 syl3anc D∞MetXSXxXySxDy*
8 eqid ySxDy=ySxDy
9 7 8 fmptd D∞MetXSXxXySxDy:S*
10 9 frnd D∞MetXSXxXranySxDy*
11 infxrcl ranySxDy*supranySxDy*<*
12 10 11 syl D∞MetXSXxXsupranySxDy*<*
13 xmetge0 D∞MetXxXyX0xDy
14 2 3 5 13 syl3anc D∞MetXSXxXyS0xDy
15 14 ralrimiva D∞MetXSXxXyS0xDy
16 ovex xDyV
17 16 rgenw ySxDyV
18 breq2 z=xDy0z0xDy
19 8 18 ralrnmptw ySxDyVzranySxDy0zyS0xDy
20 17 19 ax-mp zranySxDy0zyS0xDy
21 15 20 sylibr D∞MetXSXxXzranySxDy0z
22 0xr 0*
23 infxrgelb ranySxDy*0*0supranySxDy*<zranySxDy0z
24 10 22 23 sylancl D∞MetXSXxX0supranySxDy*<zranySxDy0z
25 21 24 mpbird D∞MetXSXxX0supranySxDy*<
26 elxrge0 supranySxDy*<0+∞supranySxDy*<*0supranySxDy*<
27 12 25 26 sylanbrc D∞MetXSXxXsupranySxDy*<0+∞
28 27 1 fmptd D∞MetXSXF:X0+∞