Metamath Proof Explorer

Theorem metdscn2

Description: The function F which gives the distance from a point to a nonempty set in a metric space is a continuous function into the topology of the complex numbers. (Contributed by Mario Carneiro, 5-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 )
metdscn2.k 
|- K = ( TopOpen ` CCfld )
Assertion metdscn2 
|- ( ( D e. ( Met ` X ) /\ S C_ X /\ S =/= (/) ) -> 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 metdscn2.k 
 |-  K = ( TopOpen ` CCfld )
4 eqid 
 |-  ( dist ` RR*s ) = ( dist ` RR*s )
5 4 xrsdsre 
 |-  ( ( dist ` RR*s ) |` ( RR X. RR ) ) = ( ( abs o. - ) |` ( RR X. RR ) )
6 4 xrsxmet 
 |-  ( dist ` RR*s ) e. ( *Met ` RR* )
7 ressxr 
 |-  RR C_ RR*
8 eqid 
 |-  ( ( dist ` RR*s ) |` ( RR X. RR ) ) = ( ( dist ` RR*s ) |` ( RR X. RR ) )
9 eqid 
 |-  ( MetOpen ` ( dist ` RR*s ) ) = ( MetOpen ` ( dist ` RR*s ) )
10 eqid 
 |-  ( MetOpen ` ( ( dist ` RR*s ) |` ( RR X. RR ) ) ) = ( MetOpen ` ( ( dist ` RR*s ) |` ( RR X. RR ) ) )
11 8 9 10 metrest 
 |-  ( ( ( dist ` RR*s ) e. ( *Met ` RR* ) /\ RR C_ RR* ) -> ( ( MetOpen ` ( dist ` RR*s ) ) |`t RR ) = ( MetOpen ` ( ( dist ` RR*s ) |` ( RR X. RR ) ) ) )
12 6 7 11 mp2an 
 |-  ( ( MetOpen ` ( dist ` RR*s ) ) |`t RR ) = ( MetOpen ` ( ( dist ` RR*s ) |` ( RR X. RR ) ) )
13 5 12 tgioo 
 |-  ( topGen ` ran (,) ) = ( ( MetOpen ` ( dist ` RR*s ) ) |`t RR )
14 3 tgioo2 
 |-  ( topGen ` ran (,) ) = ( K |`t RR )
15 13 14 eqtr3i 
 |-  ( ( MetOpen ` ( dist ` RR*s ) ) |`t RR ) = ( K |`t RR )
16 15 oveq2i 
 |-  ( J Cn ( ( MetOpen ` ( dist ` RR*s ) ) |`t RR ) ) = ( J Cn ( K |`t RR ) )
17 3 cnfldtop 
 |-  K e. Top
18 cnrest2r 
 |-  ( K e. Top -> ( J Cn ( K |`t RR ) ) C_ ( J Cn K ) )
19 17 18 ax-mp 
 |-  ( J Cn ( K |`t RR ) ) C_ ( J Cn K )
20 16 19 eqsstri 
 |-  ( J Cn ( ( MetOpen ` ( dist ` RR*s ) ) |`t RR ) ) C_ ( J Cn K )
21 metxmet 
 |-  ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
22 1 2 4 9 metdscn 
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X ) -> F e. ( J Cn ( MetOpen ` ( dist ` RR*s ) ) ) )
23 21 22 sylan 
 |-  ( ( D e. ( Met ` X ) /\ S C_ X ) -> F e. ( J Cn ( MetOpen ` ( dist ` RR*s ) ) ) )
24 23 3adant3 
 |-  ( ( D e. ( Met ` X ) /\ S C_ X /\ S =/= (/) ) -> F e. ( J Cn ( MetOpen ` ( dist ` RR*s ) ) ) )
25 1 metdsre 
 |-  ( ( D e. ( Met ` X ) /\ S C_ X /\ S =/= (/) ) -> F : X --> RR )
26 frn 
 |-  ( F : X --> RR -> ran F C_ RR )
27 9 mopntopon 
 |-  ( ( dist ` RR*s ) e. ( *Met ` RR* ) -> ( MetOpen ` ( dist ` RR*s ) ) e. ( TopOn ` RR* ) )
28 6 27 ax-mp 
 |-  ( MetOpen ` ( dist ` RR*s ) ) e. ( TopOn ` RR* )
29 cnrest2 
 |-  ( ( ( MetOpen ` ( dist ` RR*s ) ) e. ( TopOn ` RR* ) /\ ran F C_ RR /\ RR C_ RR* ) -> ( F e. ( J Cn ( MetOpen ` ( dist ` RR*s ) ) ) <-> F e. ( J Cn ( ( MetOpen ` ( dist ` RR*s ) ) |`t RR ) ) ) )
30 28 7 29 mp3an13 
 |-  ( ran F C_ RR -> ( F e. ( J Cn ( MetOpen ` ( dist ` RR*s ) ) ) <-> F e. ( J Cn ( ( MetOpen ` ( dist ` RR*s ) ) |`t RR ) ) ) )
31 25 26 30 3syl 
 |-  ( ( D e. ( Met ` X ) /\ S C_ X /\ S =/= (/) ) -> ( F e. ( J Cn ( MetOpen ` ( dist ` RR*s ) ) ) <-> F e. ( J Cn ( ( MetOpen ` ( dist ` RR*s ) ) |`t RR ) ) ) )
32 24 31 mpbid 
 |-  ( ( D e. ( Met ` X ) /\ S C_ X /\ S =/= (/) ) -> F e. ( J Cn ( ( MetOpen ` ( dist ` RR*s ) ) |`t RR ) ) )
33 20 32 sselid 
 |-  ( ( D e. ( Met ` X ) /\ S C_ X /\ S =/= (/) ) -> F e. ( J Cn K ) )