Metamath Proof Explorer

Theorem metdsf

Description: The distance from a point to a set is a nonnegative extended real number. (Contributed by Mario Carneiro, 14-Feb-2015) (Revised by Mario Carneiro, 4-Sep-2015) (Proof shortened by AV, 30-Sep-2020)

Ref Expression
Hypothesis metdscn.f 
|- F = ( x e. X |-> inf ( ran ( y e. S |-> ( x D y ) ) , RR* , < ) )
Assertion metdsf 
|- ( ( D e. ( *Met ` X ) /\ S C_ X ) -> F : X --> ( 0 [,] +oo ) )

Proof

Step Hyp Ref Expression
1 metdscn.f 
 |-  F = ( x e. X |-> inf ( ran ( y e. S |-> ( x D y ) ) , RR* , < ) )
2 simplll 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ x e. X ) /\ y e. S ) -> D e. ( *Met ` X ) )
3 simplr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ x e. X ) /\ y e. S ) -> x e. X )
4 simplr 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ x e. X ) -> S C_ X )
5 4 sselda 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ x e. X ) /\ y e. S ) -> y e. X )
6 xmetcl 
 |-  ( ( D e. ( *Met ` X ) /\ x e. X /\ y e. X ) -> ( x D y ) e. RR* )
7 2 3 5 6 syl3anc 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ x e. X ) /\ y e. S ) -> ( x D y ) e. RR* )
8 eqid 
 |-  ( y e. S |-> ( x D y ) ) = ( y e. S |-> ( x D y ) )
9 7 8 fmptd 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ x e. X ) -> ( y e. S |-> ( x D y ) ) : S --> RR* )
10 9 frnd 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ x e. X ) -> ran ( y e. S |-> ( x D y ) ) C_ RR* )
11 infxrcl 
 |-  ( ran ( y e. S |-> ( x D y ) ) C_ RR* -> inf ( ran ( y e. S |-> ( x D y ) ) , RR* , < ) e. RR* )
12 10 11 syl 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ x e. X ) -> inf ( ran ( y e. S |-> ( x D y ) ) , RR* , < ) e. RR* )
13 xmetge0 
 |-  ( ( D e. ( *Met ` X ) /\ x e. X /\ y e. X ) -> 0 <_ ( x D y ) )
14 2 3 5 13 syl3anc 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ x e. X ) /\ y e. S ) -> 0 <_ ( x D y ) )
15 14 ralrimiva 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ x e. X ) -> A. y e. S 0 <_ ( x D y ) )
16 ovex 
 |-  ( x D y ) e. _V
17 16 rgenw 
 |-  A. y e. S ( x D y ) e. _V
18 breq2 
 |-  ( z = ( x D y ) -> ( 0 <_ z <-> 0 <_ ( x D y ) ) )
19 8 18 ralrnmptw 
 |-  ( A. y e. S ( x D y ) e. _V -> ( A. z e. ran ( y e. S |-> ( x D y ) ) 0 <_ z <-> A. y e. S 0 <_ ( x D y ) ) )
20 17 19 ax-mp 
 |-  ( A. z e. ran ( y e. S |-> ( x D y ) ) 0 <_ z <-> A. y e. S 0 <_ ( x D y ) )
21 15 20 sylibr 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ x e. X ) -> A. z e. ran ( y e. S |-> ( x D y ) ) 0 <_ z )
22 0xr 
 |-  0 e. RR*
23 infxrgelb 
 |-  ( ( ran ( y e. S |-> ( x D y ) ) C_ RR* /\ 0 e. RR* ) -> ( 0 <_ inf ( ran ( y e. S |-> ( x D y ) ) , RR* , < ) <-> A. z e. ran ( y e. S |-> ( x D y ) ) 0 <_ z ) )
24 10 22 23 sylancl 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ x e. X ) -> ( 0 <_ inf ( ran ( y e. S |-> ( x D y ) ) , RR* , < ) <-> A. z e. ran ( y e. S |-> ( x D y ) ) 0 <_ z ) )
25 21 24 mpbird 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ x e. X ) -> 0 <_ inf ( ran ( y e. S |-> ( x D y ) ) , RR* , < ) )
26 elxrge0 
 |-  ( inf ( ran ( y e. S |-> ( x D y ) ) , RR* , < ) e. ( 0 [,] +oo ) <-> ( inf ( ran ( y e. S |-> ( x D y ) ) , RR* , < ) e. RR* /\ 0 <_ inf ( ran ( y e. S |-> ( x D y ) ) , RR* , < ) ) )
27 12 25 26 sylanbrc 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ x e. X ) -> inf ( ran ( y e. S |-> ( x D y ) ) , RR* , < ) e. ( 0 [,] +oo ) )
28 27 1 fmptd 
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X ) -> F : X --> ( 0 [,] +oo ) )