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

Proof

Step Hyp Ref Expression
1 metdscn.f
 |-  F = ( x e. X |-> inf ( ran ( y e. S |-> ( x D y ) ) , RR* , < ) )
2 1 metdsf
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X ) -> F : X --> ( 0 [,] +oo ) )
3 2 3adant3
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) -> F : X --> ( 0 [,] +oo ) )
4 ssel2
 |-  ( ( S C_ X /\ A e. S ) -> A e. X )
5 4 3adant1
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) -> A e. X )
6 3 5 ffvelrnd
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) -> ( F ` A ) e. ( 0 [,] +oo ) )
7 eliccxr
 |-  ( ( F ` A ) e. ( 0 [,] +oo ) -> ( F ` A ) e. RR* )
8 6 7 syl
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) -> ( F ` A ) e. RR* )
9 8 xrleidd
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) -> ( F ` A ) <_ ( F ` A ) )
10 simp1
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) -> D e. ( *Met ` X ) )
11 simp2
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) -> S C_ X )
12 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 ) ) ) = (/) ) )
13 10 11 5 8 12 syl31anc
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) -> ( ( F ` A ) <_ ( F ` A ) <-> ( S i^i ( A ( ball ` D ) ( F ` A ) ) ) = (/) ) )
14 9 13 mpbid
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) -> ( S i^i ( A ( ball ` D ) ( F ` A ) ) ) = (/) )
15 simpl3
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) /\ 0 < ( F ` A ) ) -> A e. S )
16 10 adantr
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) /\ 0 < ( F ` A ) ) -> D e. ( *Met ` X ) )
17 5 adantr
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) /\ 0 < ( F ` A ) ) -> A e. X )
18 8 adantr
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) /\ 0 < ( F ` A ) ) -> ( F ` A ) e. RR* )
19 simpr
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) /\ 0 < ( F ` A ) ) -> 0 < ( F ` A ) )
20 xblcntr
 |-  ( ( D e. ( *Met ` X ) /\ A e. X /\ ( ( F ` A ) e. RR* /\ 0 < ( F ` A ) ) ) -> A e. ( A ( ball ` D ) ( F ` A ) ) )
21 16 17 18 19 20 syl112anc
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) /\ 0 < ( F ` A ) ) -> A e. ( A ( ball ` D ) ( F ` A ) ) )
22 inelcm
 |-  ( ( A e. S /\ A e. ( A ( ball ` D ) ( F ` A ) ) ) -> ( S i^i ( A ( ball ` D ) ( F ` A ) ) ) =/= (/) )
23 15 21 22 syl2anc
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) /\ 0 < ( F ` A ) ) -> ( S i^i ( A ( ball ` D ) ( F ` A ) ) ) =/= (/) )
24 23 ex
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) -> ( 0 < ( F ` A ) -> ( S i^i ( A ( ball ` D ) ( F ` A ) ) ) =/= (/) ) )
25 24 necon2bd
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) -> ( ( S i^i ( A ( ball ` D ) ( F ` A ) ) ) = (/) -> -. 0 < ( F ` A ) ) )
26 14 25 mpd
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) -> -. 0 < ( F ` A ) )
27 elxrge0
 |-  ( ( F ` A ) e. ( 0 [,] +oo ) <-> ( ( F ` A ) e. RR* /\ 0 <_ ( F ` A ) ) )
28 27 simprbi
 |-  ( ( F ` A ) e. ( 0 [,] +oo ) -> 0 <_ ( F ` A ) )
29 6 28 syl
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) -> 0 <_ ( F ` A ) )
30 0xr
 |-  0 e. RR*
31 xrleloe
 |-  ( ( 0 e. RR* /\ ( F ` A ) e. RR* ) -> ( 0 <_ ( F ` A ) <-> ( 0 < ( F ` A ) \/ 0 = ( F ` A ) ) ) )
32 30 8 31 sylancr
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) -> ( 0 <_ ( F ` A ) <-> ( 0 < ( F ` A ) \/ 0 = ( F ` A ) ) ) )
33 29 32 mpbid
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) -> ( 0 < ( F ` A ) \/ 0 = ( F ` A ) ) )
34 33 ord
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) -> ( -. 0 < ( F ` A ) -> 0 = ( F ` A ) ) )
35 26 34 mpd
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) -> 0 = ( F ` A ) )
36 35 eqcomd
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) -> ( F ` A ) = 0 )