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 | |
|
Assertion | metdsf | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | metdscn.f | |
|
2 | simplll | |
|
3 | simplr | |
|
4 | simplr | |
|
5 | 4 | sselda | |
6 | xmetcl | |
|
7 | 2 3 5 6 | syl3anc | |
8 | eqid | |
|
9 | 7 8 | fmptd | |
10 | 9 | frnd | |
11 | infxrcl | |
|
12 | 10 11 | syl | |
13 | xmetge0 | |
|
14 | 2 3 5 13 | syl3anc | |
15 | 14 | ralrimiva | |
16 | ovex | |
|
17 | 16 | rgenw | |
18 | breq2 | |
|
19 | 8 18 | ralrnmptw | |
20 | 17 19 | ax-mp | |
21 | 15 20 | sylibr | |
22 | 0xr | |
|
23 | infxrgelb | |
|
24 | 10 22 23 | sylancl | |
25 | 21 24 | mpbird | |
26 | elxrge0 | |
|
27 | 12 25 26 | sylanbrc | |
28 | 27 1 | fmptd | |