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 ) )