Metamath Proof Explorer


Theorem metds0

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 F=xXsupranySxDy*<
Assertion metds0 D∞MetXSXASFA=0

Proof

Step Hyp Ref Expression
1 metdscn.f F=xXsupranySxDy*<
2 1 metdsf D∞MetXSXF:X0+∞
3 2 3adant3 D∞MetXSXASF:X0+∞
4 ssel2 SXASAX
5 4 3adant1 D∞MetXSXASAX
6 3 5 ffvelrnd D∞MetXSXASFA0+∞
7 eliccxr FA0+∞FA*
8 6 7 syl D∞MetXSXASFA*
9 8 xrleidd D∞MetXSXASFAFA
10 simp1 D∞MetXSXASD∞MetX
11 simp2 D∞MetXSXASSX
12 1 metdsge D∞MetXSXAXFA*FAFASAballDFA=
13 10 11 5 8 12 syl31anc D∞MetXSXASFAFASAballDFA=
14 9 13 mpbid D∞MetXSXASSAballDFA=
15 simpl3 D∞MetXSXAS0<FAAS
16 10 adantr D∞MetXSXAS0<FAD∞MetX
17 5 adantr D∞MetXSXAS0<FAAX
18 8 adantr D∞MetXSXAS0<FAFA*
19 simpr D∞MetXSXAS0<FA0<FA
20 xblcntr D∞MetXAXFA*0<FAAAballDFA
21 16 17 18 19 20 syl112anc D∞MetXSXAS0<FAAAballDFA
22 inelcm ASAAballDFASAballDFA
23 15 21 22 syl2anc D∞MetXSXAS0<FASAballDFA
24 23 ex D∞MetXSXAS0<FASAballDFA
25 24 necon2bd D∞MetXSXASSAballDFA=¬0<FA
26 14 25 mpd D∞MetXSXAS¬0<FA
27 elxrge0 FA0+∞FA*0FA
28 27 simprbi FA0+∞0FA
29 6 28 syl D∞MetXSXAS0FA
30 0xr 0*
31 xrleloe 0*FA*0FA0<FA0=FA
32 30 8 31 sylancr D∞MetXSXAS0FA0<FA0=FA
33 29 32 mpbid D∞MetXSXAS0<FA0=FA
34 33 ord D∞MetXSXAS¬0<FA0=FA
35 26 34 mpd D∞MetXSXAS0=FA
36 35 eqcomd D∞MetXSXASFA=0