Metamath Proof Explorer


Theorem metdscn

Description: The function F which gives the distance from a point to a set is a continuous function into the metric topology of the extended reals. (Contributed by Mario Carneiro, 14-Feb-2015) (Revised by Mario Carneiro, 4-Sep-2015)

Ref Expression
Hypotheses metdscn.f
|- F = ( x e. X |-> inf ( ran ( y e. S |-> ( x D y ) ) , RR* , < ) )
metdscn.j
|- J = ( MetOpen ` D )
metdscn.c
|- C = ( dist ` RR*s )
metdscn.k
|- K = ( MetOpen ` C )
Assertion metdscn
|- ( ( D e. ( *Met ` X ) /\ S C_ X ) -> F e. ( J Cn K ) )

Proof

Step Hyp Ref Expression
1 metdscn.f
 |-  F = ( x e. X |-> inf ( ran ( y e. S |-> ( x D y ) ) , RR* , < ) )
2 metdscn.j
 |-  J = ( MetOpen ` D )
3 metdscn.c
 |-  C = ( dist ` RR*s )
4 metdscn.k
 |-  K = ( MetOpen ` C )
5 1 metdsf
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X ) -> F : X --> ( 0 [,] +oo ) )
6 iccssxr
 |-  ( 0 [,] +oo ) C_ RR*
7 fss
 |-  ( ( F : X --> ( 0 [,] +oo ) /\ ( 0 [,] +oo ) C_ RR* ) -> F : X --> RR* )
8 5 6 7 sylancl
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X ) -> F : X --> RR* )
9 simprr
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( z e. X /\ r e. RR+ ) ) -> r e. RR+ )
10 8 ad2antrr
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( z e. X /\ r e. RR+ ) ) /\ ( w e. X /\ ( z D w ) < r ) ) -> F : X --> RR* )
11 simplrl
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( z e. X /\ r e. RR+ ) ) /\ ( w e. X /\ ( z D w ) < r ) ) -> z e. X )
12 10 11 ffvelrnd
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( z e. X /\ r e. RR+ ) ) /\ ( w e. X /\ ( z D w ) < r ) ) -> ( F ` z ) e. RR* )
13 simprl
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( z e. X /\ r e. RR+ ) ) /\ ( w e. X /\ ( z D w ) < r ) ) -> w e. X )
14 10 13 ffvelrnd
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( z e. X /\ r e. RR+ ) ) /\ ( w e. X /\ ( z D w ) < r ) ) -> ( F ` w ) e. RR* )
15 3 xrsdsval
 |-  ( ( ( F ` z ) e. RR* /\ ( F ` w ) e. RR* ) -> ( ( F ` z ) C ( F ` w ) ) = if ( ( F ` z ) <_ ( F ` w ) , ( ( F ` w ) +e -e ( F ` z ) ) , ( ( F ` z ) +e -e ( F ` w ) ) ) )
16 12 14 15 syl2anc
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( z e. X /\ r e. RR+ ) ) /\ ( w e. X /\ ( z D w ) < r ) ) -> ( ( F ` z ) C ( F ` w ) ) = if ( ( F ` z ) <_ ( F ` w ) , ( ( F ` w ) +e -e ( F ` z ) ) , ( ( F ` z ) +e -e ( F ` w ) ) ) )
17 simplll
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( z e. X /\ r e. RR+ ) ) /\ ( w e. X /\ ( z D w ) < r ) ) -> D e. ( *Met ` X ) )
18 simpllr
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( z e. X /\ r e. RR+ ) ) /\ ( w e. X /\ ( z D w ) < r ) ) -> S C_ X )
19 simplrr
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( z e. X /\ r e. RR+ ) ) /\ ( w e. X /\ ( z D w ) < r ) ) -> r e. RR+ )
20 xmetsym
 |-  ( ( D e. ( *Met ` X ) /\ w e. X /\ z e. X ) -> ( w D z ) = ( z D w ) )
21 17 13 11 20 syl3anc
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( z e. X /\ r e. RR+ ) ) /\ ( w e. X /\ ( z D w ) < r ) ) -> ( w D z ) = ( z D w ) )
22 simprr
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( z e. X /\ r e. RR+ ) ) /\ ( w e. X /\ ( z D w ) < r ) ) -> ( z D w ) < r )
23 21 22 eqbrtrd
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( z e. X /\ r e. RR+ ) ) /\ ( w e. X /\ ( z D w ) < r ) ) -> ( w D z ) < r )
24 1 2 3 4 17 18 13 11 19 23 metdscnlem
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( z e. X /\ r e. RR+ ) ) /\ ( w e. X /\ ( z D w ) < r ) ) -> ( ( F ` w ) +e -e ( F ` z ) ) < r )
25 1 2 3 4 17 18 11 13 19 22 metdscnlem
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( z e. X /\ r e. RR+ ) ) /\ ( w e. X /\ ( z D w ) < r ) ) -> ( ( F ` z ) +e -e ( F ` w ) ) < r )
26 breq1
 |-  ( ( ( F ` w ) +e -e ( F ` z ) ) = if ( ( F ` z ) <_ ( F ` w ) , ( ( F ` w ) +e -e ( F ` z ) ) , ( ( F ` z ) +e -e ( F ` w ) ) ) -> ( ( ( F ` w ) +e -e ( F ` z ) ) < r <-> if ( ( F ` z ) <_ ( F ` w ) , ( ( F ` w ) +e -e ( F ` z ) ) , ( ( F ` z ) +e -e ( F ` w ) ) ) < r ) )
27 breq1
 |-  ( ( ( F ` z ) +e -e ( F ` w ) ) = if ( ( F ` z ) <_ ( F ` w ) , ( ( F ` w ) +e -e ( F ` z ) ) , ( ( F ` z ) +e -e ( F ` w ) ) ) -> ( ( ( F ` z ) +e -e ( F ` w ) ) < r <-> if ( ( F ` z ) <_ ( F ` w ) , ( ( F ` w ) +e -e ( F ` z ) ) , ( ( F ` z ) +e -e ( F ` w ) ) ) < r ) )
28 26 27 ifboth
 |-  ( ( ( ( F ` w ) +e -e ( F ` z ) ) < r /\ ( ( F ` z ) +e -e ( F ` w ) ) < r ) -> if ( ( F ` z ) <_ ( F ` w ) , ( ( F ` w ) +e -e ( F ` z ) ) , ( ( F ` z ) +e -e ( F ` w ) ) ) < r )
29 24 25 28 syl2anc
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( z e. X /\ r e. RR+ ) ) /\ ( w e. X /\ ( z D w ) < r ) ) -> if ( ( F ` z ) <_ ( F ` w ) , ( ( F ` w ) +e -e ( F ` z ) ) , ( ( F ` z ) +e -e ( F ` w ) ) ) < r )
30 16 29 eqbrtrd
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( z e. X /\ r e. RR+ ) ) /\ ( w e. X /\ ( z D w ) < r ) ) -> ( ( F ` z ) C ( F ` w ) ) < r )
31 30 expr
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( z e. X /\ r e. RR+ ) ) /\ w e. X ) -> ( ( z D w ) < r -> ( ( F ` z ) C ( F ` w ) ) < r ) )
32 31 ralrimiva
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( z e. X /\ r e. RR+ ) ) -> A. w e. X ( ( z D w ) < r -> ( ( F ` z ) C ( F ` w ) ) < r ) )
33 breq2
 |-  ( s = r -> ( ( z D w ) < s <-> ( z D w ) < r ) )
34 33 rspceaimv
 |-  ( ( r e. RR+ /\ A. w e. X ( ( z D w ) < r -> ( ( F ` z ) C ( F ` w ) ) < r ) ) -> E. s e. RR+ A. w e. X ( ( z D w ) < s -> ( ( F ` z ) C ( F ` w ) ) < r ) )
35 9 32 34 syl2anc
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( z e. X /\ r e. RR+ ) ) -> E. s e. RR+ A. w e. X ( ( z D w ) < s -> ( ( F ` z ) C ( F ` w ) ) < r ) )
36 35 ralrimivva
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X ) -> A. z e. X A. r e. RR+ E. s e. RR+ A. w e. X ( ( z D w ) < s -> ( ( F ` z ) C ( F ` w ) ) < r ) )
37 simpl
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X ) -> D e. ( *Met ` X ) )
38 3 xrsxmet
 |-  C e. ( *Met ` RR* )
39 2 4 metcn
 |-  ( ( D e. ( *Met ` X ) /\ C e. ( *Met ` RR* ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> RR* /\ A. z e. X A. r e. RR+ E. s e. RR+ A. w e. X ( ( z D w ) < s -> ( ( F ` z ) C ( F ` w ) ) < r ) ) ) )
40 37 38 39 sylancl
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X ) -> ( F e. ( J Cn K ) <-> ( F : X --> RR* /\ A. z e. X A. r e. RR+ E. s e. RR+ A. w e. X ( ( z D w ) < s -> ( ( F ` z ) C ( F ` w ) ) < r ) ) ) )
41 8 36 40 mpbir2and
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X ) -> F e. ( J Cn K ) )