Metamath Proof Explorer


Theorem metdseq0

Description: The distance from a point to a set is zero iff the point is in the closure set. (Contributed by Mario Carneiro, 14-Feb-2015)

Ref Expression
Hypotheses metdscn.f F = x X sup ran y S x D y * <
metdscn.j J = MetOpen D
Assertion metdseq0 D ∞Met X S X A X F A = 0 A cls J S

Proof

Step Hyp Ref Expression
1 metdscn.f F = x X sup ran y S x D y * <
2 metdscn.j J = MetOpen D
3 simpll1 D ∞Met X S X A X F A = 0 z J A z D ∞Met X
4 simprl D ∞Met X S X A X F A = 0 z J A z z J
5 simprr D ∞Met X S X A X F A = 0 z J A z A z
6 2 mopni2 D ∞Met X z J A z r + A ball D r z
7 3 4 5 6 syl3anc D ∞Met X S X A X F A = 0 z J A z r + A ball D r z
8 simprr D ∞Met X S X A X F A = 0 z J A z r + A ball D r z A ball D r z
9 8 ssrind D ∞Met X S X A X F A = 0 z J A z r + A ball D r z A ball D r S z S
10 rpgt0 r + 0 < r
11 0re 0
12 rpre r + r
13 ltnle 0 r 0 < r ¬ r 0
14 11 12 13 sylancr r + 0 < r ¬ r 0
15 10 14 mpbid r + ¬ r 0
16 15 ad2antrl D ∞Met X S X A X F A = 0 z J A z r + A ball D r z ¬ r 0
17 simpllr D ∞Met X S X A X F A = 0 z J A z r + A ball D r z F A = 0
18 17 breq2d D ∞Met X S X A X F A = 0 z J A z r + A ball D r z r F A r 0
19 3 adantr D ∞Met X S X A X F A = 0 z J A z r + A ball D r z D ∞Met X
20 simpl2 D ∞Met X S X A X F A = 0 S X
21 20 ad2antrr D ∞Met X S X A X F A = 0 z J A z r + A ball D r z S X
22 simpl3 D ∞Met X S X A X F A = 0 A X
23 22 ad2antrr D ∞Met X S X A X F A = 0 z J A z r + A ball D r z A X
24 rpxr r + r *
25 24 ad2antrl D ∞Met X S X A X F A = 0 z J A z r + A ball D r z r *
26 1 metdsge D ∞Met X S X A X r * r F A S A ball D r =
27 19 21 23 25 26 syl31anc D ∞Met X S X A X F A = 0 z J A z r + A ball D r z r F A S A ball D r =
28 18 27 bitr3d D ∞Met X S X A X F A = 0 z J A z r + A ball D r z r 0 S A ball D r =
29 incom S A ball D r = A ball D r S
30 29 eqeq1i S A ball D r = A ball D r S =
31 28 30 bitrdi D ∞Met X S X A X F A = 0 z J A z r + A ball D r z r 0 A ball D r S =
32 31 necon3bbid D ∞Met X S X A X F A = 0 z J A z r + A ball D r z ¬ r 0 A ball D r S
33 16 32 mpbid D ∞Met X S X A X F A = 0 z J A z r + A ball D r z A ball D r S
34 ssn0 A ball D r S z S A ball D r S z S
35 9 33 34 syl2anc D ∞Met X S X A X F A = 0 z J A z r + A ball D r z z S
36 7 35 rexlimddv D ∞Met X S X A X F A = 0 z J A z z S
37 36 expr D ∞Met X S X A X F A = 0 z J A z z S
38 37 ralrimiva D ∞Met X S X A X F A = 0 z J A z z S
39 2 mopntopon D ∞Met X J TopOn X
40 39 3ad2ant1 D ∞Met X S X A X J TopOn X
41 40 adantr D ∞Met X S X A X F A = 0 J TopOn X
42 topontop J TopOn X J Top
43 41 42 syl D ∞Met X S X A X F A = 0 J Top
44 toponuni J TopOn X X = J
45 41 44 syl D ∞Met X S X A X F A = 0 X = J
46 20 45 sseqtrd D ∞Met X S X A X F A = 0 S J
47 22 45 eleqtrd D ∞Met X S X A X F A = 0 A J
48 eqid J = J
49 48 elcls J Top S J A J A cls J S z J A z z S
50 43 46 47 49 syl3anc D ∞Met X S X A X F A = 0 A cls J S z J A z z S
51 38 50 mpbird D ∞Met X S X A X F A = 0 A cls J S
52 incom A ball D F A S = S A ball D F A
53 1 metdsf D ∞Met X S X F : X 0 +∞
54 53 ffvelrnda D ∞Met X S X A X F A 0 +∞
55 54 3impa D ∞Met X S X A X F A 0 +∞
56 eliccxr F A 0 +∞ F A *
57 55 56 syl D ∞Met X S X A X F A *
58 57 xrleidd D ∞Met X S X A X F A F A
59 1 metdsge D ∞Met X S X A X F A * F A F A S A ball D F A =
60 57 59 mpdan D ∞Met X S X A X F A F A S A ball D F A =
61 58 60 mpbid D ∞Met X S X A X S A ball D F A =
62 52 61 syl5eq D ∞Met X S X A X A ball D F A S =
63 62 adantr D ∞Met X S X A X A cls J S A ball D F A S =
64 40 ad2antrr D ∞Met X S X A X A cls J S 0 < F A J TopOn X
65 64 42 syl D ∞Met X S X A X A cls J S 0 < F A J Top
66 simpll2 D ∞Met X S X A X A cls J S 0 < F A S X
67 64 44 syl D ∞Met X S X A X A cls J S 0 < F A X = J
68 66 67 sseqtrd D ∞Met X S X A X A cls J S 0 < F A S J
69 simplr D ∞Met X S X A X A cls J S 0 < F A A cls J S
70 simpll1 D ∞Met X S X A X A cls J S 0 < F A D ∞Met X
71 simpll3 D ∞Met X S X A X A cls J S 0 < F A A X
72 57 ad2antrr D ∞Met X S X A X A cls J S 0 < F A F A *
73 2 blopn D ∞Met X A X F A * A ball D F A J
74 70 71 72 73 syl3anc D ∞Met X S X A X A cls J S 0 < F A A ball D F A J
75 simpr D ∞Met X S X A X A cls J S 0 < F A 0 < F A
76 xblcntr D ∞Met X A X F A * 0 < F A A A ball D F A
77 70 71 72 75 76 syl112anc D ∞Met X S X A X A cls J S 0 < F A A A ball D F A
78 48 clsndisj J Top S J A cls J S A ball D F A J A A ball D F A A ball D F A S
79 65 68 69 74 77 78 syl32anc D ∞Met X S X A X A cls J S 0 < F A A ball D F A S
80 79 ex D ∞Met X S X A X A cls J S 0 < F A A ball D F A S
81 80 necon2bd D ∞Met X S X A X A cls J S A ball D F A S = ¬ 0 < F A
82 63 81 mpd D ∞Met X S X A X A cls J S ¬ 0 < F A
83 elxrge0 F A 0 +∞ F A * 0 F A
84 83 simprbi F A 0 +∞ 0 F A
85 55 84 syl D ∞Met X S X A X 0 F A
86 0xr 0 *
87 xrleloe 0 * F A * 0 F A 0 < F A 0 = F A
88 86 57 87 sylancr D ∞Met X S X A X 0 F A 0 < F A 0 = F A
89 85 88 mpbid D ∞Met X S X A X 0 < F A 0 = F A
90 89 adantr D ∞Met X S X A X A cls J S 0 < F A 0 = F A
91 90 ord D ∞Met X S X A X A cls J S ¬ 0 < F A 0 = F A
92 82 91 mpd D ∞Met X S X A X A cls J S 0 = F A
93 92 eqcomd D ∞Met X S X A X A cls J S F A = 0
94 51 93 impbida D ∞Met X S X A X F A = 0 A cls J S