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 )