Description: If a point is in a set, its distance to the set is zero. (Contributed by Mario Carneiro, 14-Feb-2015) (Revised by Mario Carneiro, 4-Sep-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | metdscn.f | |
|
Assertion | metds0 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | metdscn.f | |
|
2 | 1 | metdsf | |
3 | 2 | 3adant3 | |
4 | ssel2 | |
|
5 | 4 | 3adant1 | |
6 | 3 5 | ffvelrnd | |
7 | eliccxr | |
|
8 | 6 7 | syl | |
9 | 8 | xrleidd | |
10 | simp1 | |
|
11 | simp2 | |
|
12 | 1 | metdsge | |
13 | 10 11 5 8 12 | syl31anc | |
14 | 9 13 | mpbid | |
15 | simpl3 | |
|
16 | 10 | adantr | |
17 | 5 | adantr | |
18 | 8 | adantr | |
19 | simpr | |
|
20 | xblcntr | |
|
21 | 16 17 18 19 20 | syl112anc | |
22 | inelcm | |
|
23 | 15 21 22 | syl2anc | |
24 | 23 | ex | |
25 | 24 | necon2bd | |
26 | 14 25 | mpd | |
27 | elxrge0 | |
|
28 | 27 | simprbi | |
29 | 6 28 | syl | |
30 | 0xr | |
|
31 | xrleloe | |
|
32 | 30 8 31 | sylancr | |
33 | 29 32 | mpbid | |
34 | 33 | ord | |
35 | 26 34 | mpd | |
36 | 35 | eqcomd | |