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 e. X |-> inf ( ran ( y e. S |-> ( x D y ) ) , RR* , < ) )
metdscn.j 
|- J = ( MetOpen ` D )
Assertion metdseq0 
|- ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. X ) -> ( ( F ` A ) = 0 <-> A e. ( ( cls ` J ) ` S ) ) )

Proof

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