MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  metdscn2 Structured version   Unicode version

Theorem metdscn2 20546
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.)
Hypotheses
Ref Expression
metdscn.f  |-  F  =  ( x  e.  X  |->  sup ( ran  (
y  e.  S  |->  ( x D y ) ) ,  RR* ,  `'  <  ) )
metdscn.j  |-  J  =  ( MetOpen `  D )
metdscn2.k  |-  K  =  ( TopOpen ` fld )
Assertion
Ref Expression
metdscn2  |-  ( ( D  e.  ( Met `  X )  /\  S  C_  X  /\  S  =/=  (/) )  ->  F  e.  ( J  Cn  K
) )
Distinct variable groups:    x, y, D    y, J    x, S, y    x, X, y
Allowed substitution hints:    F( x, y)    J( x)    K( x, y)

Proof of Theorem metdscn2
StepHypRef Expression
1 eqid 2451 . . . . . . 7  |-  ( dist `  RR*s )  =  ( dist `  RR*s
)
21xrsdsre 20500 . . . . . 6  |-  ( (
dist `  RR*s )  |`  ( RR  X.  RR ) )  =  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) )
31xrsxmet 20499 . . . . . . 7  |-  ( dist `  RR*s )  e.  ( *Met `  RR* )
4 ressxr 9525 . . . . . . 7  |-  RR  C_  RR*
5 eqid 2451 . . . . . . . 8  |-  ( (
dist `  RR*s )  |`  ( RR  X.  RR ) )  =  ( ( dist `  RR*s
)  |`  ( RR  X.  RR ) )
6 eqid 2451 . . . . . . . 8  |-  ( MetOpen `  ( dist `  RR*s ) )  =  ( MetOpen `  ( dist `  RR*s ) )
7 eqid 2451 . . . . . . . 8  |-  ( MetOpen `  ( ( dist `  RR*s
)  |`  ( RR  X.  RR ) ) )  =  ( MetOpen `  ( ( dist `  RR*s )  |`  ( RR  X.  RR ) ) )
85, 6, 7metrest 20212 . . . . . . 7  |-  ( ( ( dist `  RR*s
)  e.  ( *Met `  RR* )  /\  RR  C_  RR* )  -> 
( ( MetOpen `  ( dist `  RR*s ) )t  RR )  =  ( MetOpen `  ( ( dist `  RR*s
)  |`  ( RR  X.  RR ) ) ) )
93, 4, 8mp2an 672 . . . . . 6  |-  ( (
MetOpen `  ( dist `  RR*s
) )t  RR )  =  (
MetOpen `  ( ( dist `  RR*s )  |`  ( RR  X.  RR ) ) )
102, 9tgioo 20486 . . . . 5  |-  ( topGen ` 
ran  (,) )  =  ( ( MetOpen `  ( dist ` 
RR*s ) )t  RR )
11 metdscn2.k . . . . . 6  |-  K  =  ( TopOpen ` fld )
1211tgioo2 20493 . . . . 5  |-  ( topGen ` 
ran  (,) )  =  ( Kt  RR )
1310, 12eqtr3i 2481 . . . 4  |-  ( (
MetOpen `  ( dist `  RR*s
) )t  RR )  =  ( Kt  RR )
1413oveq2i 6198 . . 3  |-  ( J  Cn  ( ( MetOpen `  ( dist `  RR*s ) )t  RR ) )  =  ( J  Cn  ( Kt  RR ) )
1511cnfldtop 20476 . . . 4  |-  K  e. 
Top
16 cnrest2r 19004 . . . 4  |-  ( K  e.  Top  ->  ( J  Cn  ( Kt  RR ) )  C_  ( J  Cn  K ) )
1715, 16ax-mp 5 . . 3  |-  ( J  Cn  ( Kt  RR ) )  C_  ( J  Cn  K )
1814, 17eqsstri 3481 . 2  |-  ( J  Cn  ( ( MetOpen `  ( dist `  RR*s ) )t  RR ) )  C_  ( J  Cn  K
)
19 metxmet 20022 . . . . 5  |-  ( D  e.  ( Met `  X
)  ->  D  e.  ( *Met `  X
) )
20 metdscn.f . . . . . 6  |-  F  =  ( x  e.  X  |->  sup ( ran  (
y  e.  S  |->  ( x D y ) ) ,  RR* ,  `'  <  ) )
21 metdscn.j . . . . . 6  |-  J  =  ( MetOpen `  D )
2220, 21, 1, 6metdscn 20545 . . . . 5  |-  ( ( D  e.  ( *Met `  X )  /\  S  C_  X
)  ->  F  e.  ( J  Cn  ( MetOpen
`  ( dist `  RR*s
) ) ) )
2319, 22sylan 471 . . . 4  |-  ( ( D  e.  ( Met `  X )  /\  S  C_  X )  ->  F  e.  ( J  Cn  ( MetOpen
`  ( dist `  RR*s
) ) ) )
24233adant3 1008 . . 3  |-  ( ( D  e.  ( Met `  X )  /\  S  C_  X  /\  S  =/=  (/) )  ->  F  e.  ( J  Cn  ( MetOpen
`  ( dist `  RR*s
) ) ) )
2520metdsre 20542 . . . 4  |-  ( ( D  e.  ( Met `  X )  /\  S  C_  X  /\  S  =/=  (/) )  ->  F : X
--> RR )
26 frn 5660 . . . 4  |-  ( F : X --> RR  ->  ran 
F  C_  RR )
276mopntopon 20127 . . . . . 6  |-  ( (
dist `  RR*s )  e.  ( *Met ` 
RR* )  ->  ( MetOpen
`  ( dist `  RR*s
) )  e.  (TopOn `  RR* ) )
283, 27ax-mp 5 . . . . 5  |-  ( MetOpen `  ( dist `  RR*s ) )  e.  (TopOn `  RR* )
29 cnrest2 19003 . . . . 5  |-  ( ( ( 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 ) ) ) )
3028, 4, 29mp3an13 1306 . . . 4  |-  ( ran 
F  C_  RR  ->  ( F  e.  ( J  Cn  ( MetOpen `  ( dist `  RR*s ) ) )  <->  F  e.  ( J  Cn  ( ( MetOpen `  ( dist `  RR*s ) )t  RR ) ) ) )
3125, 26, 303syl 20 . . 3  |-  ( ( 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 ) ) ) )
3224, 31mpbid 210 . 2  |-  ( ( D  e.  ( Met `  X )  /\  S  C_  X  /\  S  =/=  (/) )  ->  F  e.  ( J  Cn  (
( MetOpen `  ( dist ` 
RR*s ) )t  RR ) ) )
3318, 32sseldi 3449 1  |-  ( ( D  e.  ( Met `  X )  /\  S  C_  X  /\  S  =/=  (/) )  ->  F  e.  ( J  Cn  K
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ w3a 965    = wceq 1370    e. wcel 1758    =/= wne 2642    C_ wss 3423   (/)c0 3732    |-> cmpt 4445    X. cxp 4933   `'ccnv 4934   ran crn 4936    |` cres 4937   -->wf 5509   ` cfv 5513  (class class class)co 6187   supcsup 7788   RRcr 9379   RR*cxr 9515    < clt 9516   (,)cioo 11398   distcds 14346   ↾t crest 14458   TopOpenctopn 14459   topGenctg 14475   RR*scxrs 14537   *Metcxmt 17907   Metcme 17908   MetOpencmopn 17912  ℂfldccnfld 17924   Topctop 18611  TopOnctopon 18612    Cn ccn 18941
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-rep 4498  ax-sep 4508  ax-nul 4516  ax-pow 4565  ax-pr 4626  ax-un 6469  ax-cnex 9436  ax-resscn 9437  ax-1cn 9438  ax-icn 9439  ax-addcl 9440  ax-addrcl 9441  ax-mulcl 9442  ax-mulrcl 9443  ax-mulcom 9444  ax-addass 9445  ax-mulass 9446  ax-distr 9447  ax-i2m1 9448  ax-1ne0 9449  ax-1rid 9450  ax-rnegex 9451  ax-rrecex 9452  ax-cnre 9453  ax-pre-lttri 9454  ax-pre-lttrn 9455  ax-pre-ltadd 9456  ax-pre-mulgt0 9457  ax-pre-sup 9458
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2599  df-ne 2644  df-nel 2645  df-ral 2798  df-rex 2799  df-reu 2800  df-rmo 2801  df-rab 2802  df-v 3067  df-sbc 3282  df-csb 3384  df-dif 3426  df-un 3428  df-in 3430  df-ss 3437  df-pss 3439  df-nul 3733  df-if 3887  df-pw 3957  df-sn 3973  df-pr 3975  df-tp 3977  df-op 3979  df-uni 4187  df-int 4224  df-iun 4268  df-br 4388  df-opab 4446  df-mpt 4447  df-tr 4481  df-eprel 4727  df-id 4731  df-po 4736  df-so 4737  df-fr 4774  df-we 4776  df-ord 4817  df-on 4818  df-lim 4819  df-suc 4820  df-xp 4941  df-rel 4942  df-cnv 4943  df-co 4944  df-dm 4945  df-rn 4946  df-res 4947  df-ima 4948  df-iota 5476  df-fun 5515  df-fn 5516  df-f 5517  df-f1 5518  df-fo 5519  df-f1o 5520  df-fv 5521  df-riota 6148  df-ov 6190  df-oprab 6191  df-mpt2 6192  df-om 6574  df-1st 6674  df-2nd 6675  df-recs 6929  df-rdg 6963  df-1o 7017  df-oadd 7021  df-er 7198  df-ec 7200  df-map 7313  df-en 7408  df-dom 7409  df-sdom 7410  df-fin 7411  df-fi 7759  df-sup 7789  df-pnf 9518  df-mnf 9519  df-xr 9520  df-ltxr 9521  df-le 9522  df-sub 9695  df-neg 9696  df-div 10092  df-nn 10421  df-2 10478  df-3 10479  df-4 10480  df-5 10481  df-6 10482  df-7 10483  df-8 10484  df-9 10485  df-10 10486  df-n0 10678  df-z 10745  df-dec 10854  df-uz 10960  df-q 11052  df-rp 11090  df-xneg 11187  df-xadd 11188  df-xmul 11189  df-ioo 11402  df-icc 11405  df-fz 11536  df-seq 11905  df-exp 11964  df-cj 12687  df-re 12688  df-im 12689  df-sqr 12823  df-abs 12824  df-struct 14275  df-ndx 14276  df-slot 14277  df-base 14278  df-plusg 14350  df-mulr 14351  df-starv 14352  df-tset 14356  df-ple 14357  df-ds 14359  df-unif 14360  df-rest 14460  df-topn 14461  df-topgen 14481  df-xrs 14539  df-psmet 17915  df-xmet 17916  df-met 17917  df-bl 17918  df-mopn 17919  df-cnfld 17925  df-top 18616  df-bases 18618  df-topon 18619  df-topsp 18620  df-cn 18944  df-cnp 18945  df-xms 20008  df-ms 20009
This theorem is referenced by:  lebnumlem2  20647
  Copyright terms: Public domain W3C validator