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