Description: The distance from a point to a nonempty set in a proper metric space is a real number. (Contributed by Mario Carneiro, 5-Sep-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | metdscn.f | |
|
Assertion | metdsre | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | metdscn.f | |
|
2 | n0 | |
|
3 | metxmet | |
|
4 | 1 | metdsf | |
5 | 3 4 | sylan | |
6 | 5 | adantr | |
7 | 6 | ffnd | |
8 | 5 | adantr | |
9 | simprr | |
|
10 | 8 9 | ffvelrnd | |
11 | eliccxr | |
|
12 | 10 11 | syl | |
13 | simpll | |
|
14 | simpr | |
|
15 | 14 | sselda | |
16 | 15 | adantrr | |
17 | metcl | |
|
18 | 13 16 9 17 | syl3anc | |
19 | elxrge0 | |
|
20 | 19 | simprbi | |
21 | 10 20 | syl | |
22 | 1 | metdsle | |
23 | 3 22 | sylanl1 | |
24 | xrrege0 | |
|
25 | 12 18 21 23 24 | syl22anc | |
26 | 25 | anassrs | |
27 | 26 | ralrimiva | |
28 | ffnfv | |
|
29 | 7 27 28 | sylanbrc | |
30 | 29 | ex | |
31 | 30 | exlimdv | |
32 | 2 31 | syl5bi | |
33 | 32 | 3impia | |