Metamath Proof Explorer


Theorem metdsre

Description: The distance from a point to a nonempty set in a proper metric space is a real number. (Contributed by Mario Carneiro, 5-Sep-2015)

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

Proof

Step Hyp Ref Expression
1 metdscn.f
 |-  F = ( x e. X |-> inf ( ran ( y e. S |-> ( x D y ) ) , RR* , < ) )
2 n0
 |-  ( S =/= (/) <-> E. z z e. S )
3 metxmet
 |-  ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
4 1 metdsf
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X ) -> F : X --> ( 0 [,] +oo ) )
5 3 4 sylan
 |-  ( ( D e. ( Met ` X ) /\ S C_ X ) -> F : X --> ( 0 [,] +oo ) )
6 5 adantr
 |-  ( ( ( D e. ( Met ` X ) /\ S C_ X ) /\ z e. S ) -> F : X --> ( 0 [,] +oo ) )
7 6 ffnd
 |-  ( ( ( D e. ( Met ` X ) /\ S C_ X ) /\ z e. S ) -> F Fn X )
8 5 adantr
 |-  ( ( ( D e. ( Met ` X ) /\ S C_ X ) /\ ( z e. S /\ w e. X ) ) -> F : X --> ( 0 [,] +oo ) )
9 simprr
 |-  ( ( ( D e. ( Met ` X ) /\ S C_ X ) /\ ( z e. S /\ w e. X ) ) -> w e. X )
10 8 9 ffvelrnd
 |-  ( ( ( D e. ( Met ` X ) /\ S C_ X ) /\ ( z e. S /\ w e. X ) ) -> ( F ` w ) e. ( 0 [,] +oo ) )
11 eliccxr
 |-  ( ( F ` w ) e. ( 0 [,] +oo ) -> ( F ` w ) e. RR* )
12 10 11 syl
 |-  ( ( ( D e. ( Met ` X ) /\ S C_ X ) /\ ( z e. S /\ w e. X ) ) -> ( F ` w ) e. RR* )
13 simpll
 |-  ( ( ( D e. ( Met ` X ) /\ S C_ X ) /\ ( z e. S /\ w e. X ) ) -> D e. ( Met ` X ) )
14 simpr
 |-  ( ( D e. ( Met ` X ) /\ S C_ X ) -> S C_ X )
15 14 sselda
 |-  ( ( ( D e. ( Met ` X ) /\ S C_ X ) /\ z e. S ) -> z e. X )
16 15 adantrr
 |-  ( ( ( D e. ( Met ` X ) /\ S C_ X ) /\ ( z e. S /\ w e. X ) ) -> z e. X )
17 metcl
 |-  ( ( D e. ( Met ` X ) /\ z e. X /\ w e. X ) -> ( z D w ) e. RR )
18 13 16 9 17 syl3anc
 |-  ( ( ( D e. ( Met ` X ) /\ S C_ X ) /\ ( z e. S /\ w e. X ) ) -> ( z D w ) e. RR )
19 elxrge0
 |-  ( ( F ` w ) e. ( 0 [,] +oo ) <-> ( ( F ` w ) e. RR* /\ 0 <_ ( F ` w ) ) )
20 19 simprbi
 |-  ( ( F ` w ) e. ( 0 [,] +oo ) -> 0 <_ ( F ` w ) )
21 10 20 syl
 |-  ( ( ( D e. ( Met ` X ) /\ S C_ X ) /\ ( z e. S /\ w e. X ) ) -> 0 <_ ( F ` w ) )
22 1 metdsle
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( z e. S /\ w e. X ) ) -> ( F ` w ) <_ ( z D w ) )
23 3 22 sylanl1
 |-  ( ( ( D e. ( Met ` X ) /\ S C_ X ) /\ ( z e. S /\ w e. X ) ) -> ( F ` w ) <_ ( z D w ) )
24 xrrege0
 |-  ( ( ( ( F ` w ) e. RR* /\ ( z D w ) e. RR ) /\ ( 0 <_ ( F ` w ) /\ ( F ` w ) <_ ( z D w ) ) ) -> ( F ` w ) e. RR )
25 12 18 21 23 24 syl22anc
 |-  ( ( ( D e. ( Met ` X ) /\ S C_ X ) /\ ( z e. S /\ w e. X ) ) -> ( F ` w ) e. RR )
26 25 anassrs
 |-  ( ( ( ( D e. ( Met ` X ) /\ S C_ X ) /\ z e. S ) /\ w e. X ) -> ( F ` w ) e. RR )
27 26 ralrimiva
 |-  ( ( ( D e. ( Met ` X ) /\ S C_ X ) /\ z e. S ) -> A. w e. X ( F ` w ) e. RR )
28 ffnfv
 |-  ( F : X --> RR <-> ( F Fn X /\ A. w e. X ( F ` w ) e. RR ) )
29 7 27 28 sylanbrc
 |-  ( ( ( D e. ( Met ` X ) /\ S C_ X ) /\ z e. S ) -> F : X --> RR )
30 29 ex
 |-  ( ( D e. ( Met ` X ) /\ S C_ X ) -> ( z e. S -> F : X --> RR ) )
31 30 exlimdv
 |-  ( ( D e. ( Met ` X ) /\ S C_ X ) -> ( E. z z e. S -> F : X --> RR ) )
32 2 31 syl5bi
 |-  ( ( D e. ( Met ` X ) /\ S C_ X ) -> ( S =/= (/) -> F : X --> RR ) )
33 32 3impia
 |-  ( ( D e. ( Met ` X ) /\ S C_ X /\ S =/= (/) ) -> F : X --> RR )