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 )