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

Theorem cmetcuspOLD 21962
Description: The uniform space generated by a complete metric is a complete uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.) (New usage is discouraged.) (Proof modification is discouraged.)
Assertion
Ref Expression
cmetcuspOLD  |-  ( ( X  =/=  (/)  /\  D  e.  ( CMet `  X
) )  ->  (toUnifSp `  (metUnifOLD
`  D ) )  e. CUnifSp )

Proof of Theorem cmetcuspOLD
Dummy variables  x  c  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cmetmet 21894 . . . . 5  |-  ( D  e.  ( CMet `  X
)  ->  D  e.  ( Met `  X ) )
2 metxmet 21006 . . . . 5  |-  ( D  e.  ( Met `  X
)  ->  D  e.  ( *Met `  X
) )
31, 2syl 16 . . . 4  |-  ( D  e.  ( CMet `  X
)  ->  D  e.  ( *Met `  X
) )
43anim2i 567 . . 3  |-  ( ( X  =/=  (/)  /\  D  e.  ( CMet `  X
) )  ->  ( X  =/=  (/)  /\  D  e.  ( *Met `  X ) ) )
5 metuustOLD 21243 . . 3  |-  ( ( X  =/=  (/)  /\  D  e.  ( *Met `  X ) )  -> 
(metUnifOLD `  D )  e.  (UnifOn `  X ) )
6 eqid 2454 . . . 4  |-  (toUnifSp `  (metUnifOLD `  D
) )  =  (toUnifSp `  (metUnifOLD
`  D ) )
76tususp 20944 . . 3  |-  ( (metUnifOLD `  D )  e.  (UnifOn `  X )  ->  (toUnifSp `  (metUnifOLD
`  D ) )  e. UnifSp )
84, 5, 73syl 20 . 2  |-  ( ( X  =/=  (/)  /\  D  e.  ( CMet `  X
) )  ->  (toUnifSp `  (metUnifOLD
`  D ) )  e. UnifSp )
9 simpll 751 . . . . 5  |-  ( ( ( ( X  =/=  (/)  /\  D  e.  (
CMet `  X )
)  /\  c  e.  ( Fil `  ( Base `  (toUnifSp `  (metUnifOLD
`  D ) ) ) ) )  /\  c  e.  (CauFilu `  (UnifSt `  (toUnifSp `  (metUnifOLD
`  D ) ) ) ) )  -> 
( X  =/=  (/)  /\  D  e.  ( CMet `  X
) ) )
109simprd 461 . . . . . 6  |-  ( ( ( ( X  =/=  (/)  /\  D  e.  (
CMet `  X )
)  /\  c  e.  ( Fil `  ( Base `  (toUnifSp `  (metUnifOLD
`  D ) ) ) ) )  /\  c  e.  (CauFilu `  (UnifSt `  (toUnifSp `  (metUnifOLD
`  D ) ) ) ) )  ->  D  e.  ( CMet `  X ) )
113ad3antlr 728 . . . . . . 7  |-  ( ( ( ( X  =/=  (/)  /\  D  e.  (
CMet `  X )
)  /\  c  e.  ( Fil `  ( Base `  (toUnifSp `  (metUnifOLD
`  D ) ) ) ) )  /\  c  e.  (CauFilu `  (UnifSt `  (toUnifSp `  (metUnifOLD
`  D ) ) ) ) )  ->  D  e.  ( *Met `  X ) )
124, 5syl 16 . . . . . . . . . 10  |-  ( ( X  =/=  (/)  /\  D  e.  ( CMet `  X
) )  ->  (metUnifOLD `  D
)  e.  (UnifOn `  X ) )
136tusbas 20940 . . . . . . . . . . . 12  |-  ( (metUnifOLD `  D )  e.  (UnifOn `  X )  ->  X  =  ( Base `  (toUnifSp `  (metUnifOLD
`  D ) ) ) )
1413fveq2d 5852 . . . . . . . . . . 11  |-  ( (metUnifOLD `  D )  e.  (UnifOn `  X )  ->  ( Fil `  X )  =  ( Fil `  ( Base `  (toUnifSp `  (metUnifOLD `  D
) ) ) ) )
1514eleq2d 2524 . . . . . . . . . 10  |-  ( (metUnifOLD `  D )  e.  (UnifOn `  X )  ->  (
c  e.  ( Fil `  X )  <->  c  e.  ( Fil `  ( Base `  (toUnifSp `  (metUnifOLD
`  D ) ) ) ) ) )
1612, 15syl 16 . . . . . . . . 9  |-  ( ( X  =/=  (/)  /\  D  e.  ( CMet `  X
) )  ->  (
c  e.  ( Fil `  X )  <->  c  e.  ( Fil `  ( Base `  (toUnifSp `  (metUnifOLD
`  D ) ) ) ) ) )
1716biimpar 483 . . . . . . . 8  |-  ( ( ( X  =/=  (/)  /\  D  e.  ( CMet `  X
) )  /\  c  e.  ( Fil `  ( Base `  (toUnifSp `  (metUnifOLD `  D
) ) ) ) )  ->  c  e.  ( Fil `  X ) )
1817adantr 463 . . . . . . 7  |-  ( ( ( ( X  =/=  (/)  /\  D  e.  (
CMet `  X )
)  /\  c  e.  ( Fil `  ( Base `  (toUnifSp `  (metUnifOLD
`  D ) ) ) ) )  /\  c  e.  (CauFilu `  (UnifSt `  (toUnifSp `  (metUnifOLD
`  D ) ) ) ) )  -> 
c  e.  ( Fil `  X ) )
196tususs 20942 . . . . . . . . . . . . 13  |-  ( (metUnifOLD `  D )  e.  (UnifOn `  X )  ->  (metUnifOLD `  D
)  =  (UnifSt `  (toUnifSp `  (metUnifOLD
`  D ) ) ) )
2019fveq2d 5852 . . . . . . . . . . . 12  |-  ( (metUnifOLD `  D )  e.  (UnifOn `  X )  ->  (CauFilu `  (metUnifOLD `  D ) )  =  (CauFilu `  (UnifSt `  (toUnifSp `  (metUnifOLD
`  D ) ) ) ) )
2112, 20syl 16 . . . . . . . . . . 11  |-  ( ( X  =/=  (/)  /\  D  e.  ( CMet `  X
) )  ->  (CauFilu `  (metUnifOLD `  D ) )  =  (CauFilu `  (UnifSt `  (toUnifSp `  (metUnifOLD
`  D ) ) ) ) )
2221eleq2d 2524 . . . . . . . . . 10  |-  ( ( X  =/=  (/)  /\  D  e.  ( CMet `  X
) )  ->  (
c  e.  (CauFilu `  (metUnifOLD `  D
) )  <->  c  e.  (CauFilu `  (UnifSt `  (toUnifSp `  (metUnifOLD `  D
) ) ) ) ) )
2322biimpar 483 . . . . . . . . 9  |-  ( ( ( X  =/=  (/)  /\  D  e.  ( CMet `  X
) )  /\  c  e.  (CauFilu `  (UnifSt `  (toUnifSp `  (metUnifOLD
`  D ) ) ) ) )  -> 
c  e.  (CauFilu `  (metUnifOLD `  D
) ) )
2423adantlr 712 . . . . . . . 8  |-  ( ( ( ( X  =/=  (/)  /\  D  e.  (
CMet `  X )
)  /\  c  e.  ( Fil `  ( Base `  (toUnifSp `  (metUnifOLD
`  D ) ) ) ) )  /\  c  e.  (CauFilu `  (UnifSt `  (toUnifSp `  (metUnifOLD
`  D ) ) ) ) )  -> 
c  e.  (CauFilu `  (metUnifOLD `  D
) ) )
25 cfilucfil2OLD 21245 . . . . . . . . . 10  |-  ( ( X  =/=  (/)  /\  D  e.  ( *Met `  X ) )  -> 
( c  e.  (CauFilu `  (metUnifOLD
`  D ) )  <-> 
( c  e.  (
fBas `  X )  /\  A. x  e.  RR+  E. y  e.  c  ( D " ( y  X.  y ) ) 
C_  ( 0 [,) x ) ) ) )
264, 25syl 16 . . . . . . . . 9  |-  ( ( X  =/=  (/)  /\  D  e.  ( CMet `  X
) )  ->  (
c  e.  (CauFilu `  (metUnifOLD `  D
) )  <->  ( c  e.  ( fBas `  X
)  /\  A. x  e.  RR+  E. y  e.  c  ( D "
( y  X.  y
) )  C_  (
0 [,) x ) ) ) )
2726simplbda 622 . . . . . . . 8  |-  ( ( ( X  =/=  (/)  /\  D  e.  ( CMet `  X
) )  /\  c  e.  (CauFilu `  (metUnifOLD
`  D ) ) )  ->  A. x  e.  RR+  E. y  e.  c  ( D "
( y  X.  y
) )  C_  (
0 [,) x ) )
289, 24, 27syl2anc 659 . . . . . . 7  |-  ( ( ( ( X  =/=  (/)  /\  D  e.  (
CMet `  X )
)  /\  c  e.  ( Fil `  ( Base `  (toUnifSp `  (metUnifOLD
`  D ) ) ) ) )  /\  c  e.  (CauFilu `  (UnifSt `  (toUnifSp `  (metUnifOLD
`  D ) ) ) ) )  ->  A. x  e.  RR+  E. y  e.  c  ( D " ( y  X.  y
) )  C_  (
0 [,) x ) )
29 iscfil 21873 . . . . . . . 8  |-  ( D  e.  ( *Met `  X )  ->  (
c  e.  (CauFil `  D )  <->  ( c  e.  ( Fil `  X
)  /\  A. x  e.  RR+  E. y  e.  c  ( D "
( y  X.  y
) )  C_  (
0 [,) x ) ) ) )
3029biimpar 483 . . . . . . 7  |-  ( ( D  e.  ( *Met `  X )  /\  ( c  e.  ( Fil `  X
)  /\  A. x  e.  RR+  E. y  e.  c  ( D "
( y  X.  y
) )  C_  (
0 [,) x ) ) )  ->  c  e.  (CauFil `  D )
)
3111, 18, 28, 30syl12anc 1224 . . . . . 6  |-  ( ( ( ( X  =/=  (/)  /\  D  e.  (
CMet `  X )
)  /\  c  e.  ( Fil `  ( Base `  (toUnifSp `  (metUnifOLD
`  D ) ) ) ) )  /\  c  e.  (CauFilu `  (UnifSt `  (toUnifSp `  (metUnifOLD
`  D ) ) ) ) )  -> 
c  e.  (CauFil `  D ) )
32 eqid 2454 . . . . . . 7  |-  ( MetOpen `  D )  =  (
MetOpen `  D )
3332cmetcvg 21893 . . . . . 6  |-  ( ( D  e.  ( CMet `  X )  /\  c  e.  (CauFil `  D )
)  ->  ( ( MetOpen
`  D )  fLim  c )  =/=  (/) )
3410, 31, 33syl2anc 659 . . . . 5  |-  ( ( ( ( X  =/=  (/)  /\  D  e.  (
CMet `  X )
)  /\  c  e.  ( Fil `  ( Base `  (toUnifSp `  (metUnifOLD
`  D ) ) ) ) )  /\  c  e.  (CauFilu `  (UnifSt `  (toUnifSp `  (metUnifOLD
`  D ) ) ) ) )  -> 
( ( MetOpen `  D
)  fLim  c )  =/=  (/) )
35 eqid 2454 . . . . . . . . . . 11  |-  (unifTop `  (metUnifOLD `  D
) )  =  (unifTop `  (metUnifOLD
`  D ) )
366, 35tustopn 20943 . . . . . . . . . 10  |-  ( (metUnifOLD `  D )  e.  (UnifOn `  X )  ->  (unifTop `  (metUnifOLD
`  D ) )  =  ( TopOpen `  (toUnifSp `  (metUnifOLD
`  D ) ) ) )
3712, 36syl 16 . . . . . . . . 9  |-  ( ( X  =/=  (/)  /\  D  e.  ( CMet `  X
) )  ->  (unifTop `  (metUnifOLD
`  D ) )  =  ( TopOpen `  (toUnifSp `  (metUnifOLD
`  D ) ) ) )
38 metutopOLD 21254 . . . . . . . . . 10  |-  ( ( X  =/=  (/)  /\  D  e.  ( *Met `  X ) )  -> 
(unifTop `  (metUnifOLD
`  D ) )  =  ( MetOpen `  D
) )
394, 38syl 16 . . . . . . . . 9  |-  ( ( X  =/=  (/)  /\  D  e.  ( CMet `  X
) )  ->  (unifTop `  (metUnifOLD
`  D ) )  =  ( MetOpen `  D
) )
4037, 39eqtr3d 2497 . . . . . . . 8  |-  ( ( X  =/=  (/)  /\  D  e.  ( CMet `  X
) )  ->  ( TopOpen
`  (toUnifSp `  (metUnifOLD
`  D ) ) )  =  ( MetOpen `  D ) )
4140oveq1d 6285 . . . . . . 7  |-  ( ( X  =/=  (/)  /\  D  e.  ( CMet `  X
) )  ->  (
( TopOpen `  (toUnifSp `  (metUnifOLD `  D
) ) )  fLim  c )  =  ( (
MetOpen `  D )  fLim  c ) )
4241neeq1d 2731 . . . . . 6  |-  ( ( X  =/=  (/)  /\  D  e.  ( CMet `  X
) )  ->  (
( ( TopOpen `  (toUnifSp `  (metUnifOLD
`  D ) ) )  fLim  c )  =/=  (/)  <->  ( ( MetOpen `  D )  fLim  c
)  =/=  (/) ) )
4342biimpar 483 . . . . 5  |-  ( ( ( X  =/=  (/)  /\  D  e.  ( CMet `  X
) )  /\  (
( MetOpen `  D )  fLim  c )  =/=  (/) )  -> 
( ( TopOpen `  (toUnifSp `  (metUnifOLD
`  D ) ) )  fLim  c )  =/=  (/) )
449, 34, 43syl2anc 659 . . . 4  |-  ( ( ( ( X  =/=  (/)  /\  D  e.  (
CMet `  X )
)  /\  c  e.  ( Fil `  ( Base `  (toUnifSp `  (metUnifOLD
`  D ) ) ) ) )  /\  c  e.  (CauFilu `  (UnifSt `  (toUnifSp `  (metUnifOLD
`  D ) ) ) ) )  -> 
( ( TopOpen `  (toUnifSp `  (metUnifOLD
`  D ) ) )  fLim  c )  =/=  (/) )
4544ex 432 . . 3  |-  ( ( ( X  =/=  (/)  /\  D  e.  ( CMet `  X
) )  /\  c  e.  ( Fil `  ( Base `  (toUnifSp `  (metUnifOLD `  D
) ) ) ) )  ->  ( c  e.  (CauFilu `  (UnifSt `  (toUnifSp `  (metUnifOLD
`  D ) ) ) )  ->  (
( TopOpen `  (toUnifSp `  (metUnifOLD `  D
) ) )  fLim  c )  =/=  (/) ) )
4645ralrimiva 2868 . 2  |-  ( ( X  =/=  (/)  /\  D  e.  ( CMet `  X
) )  ->  A. c  e.  ( Fil `  ( Base `  (toUnifSp `  (metUnifOLD `  D
) ) ) ) ( c  e.  (CauFilu `  (UnifSt `  (toUnifSp `  (metUnifOLD `  D
) ) ) )  ->  ( ( TopOpen `  (toUnifSp `  (metUnifOLD
`  D ) ) )  fLim  c )  =/=  (/) ) )
47 iscusp 20971 . 2  |-  ( (toUnifSp `  (metUnifOLD
`  D ) )  e. CUnifSp 
<->  ( (toUnifSp `  (metUnifOLD `  D
) )  e. UnifSp  /\  A. c  e.  ( Fil `  ( Base `  (toUnifSp `  (metUnifOLD
`  D ) ) ) ) ( c  e.  (CauFilu `  (UnifSt `  (toUnifSp `  (metUnifOLD
`  D ) ) ) )  ->  (
( TopOpen `  (toUnifSp `  (metUnifOLD `  D
) ) )  fLim  c )  =/=  (/) ) ) )
488, 46, 47sylanbrc 662 1  |-  ( ( X  =/=  (/)  /\  D  e.  ( CMet `  X
) )  ->  (toUnifSp `  (metUnifOLD
`  D ) )  e. CUnifSp )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367    = wceq 1398    e. wcel 1823    =/= wne 2649   A.wral 2804   E.wrex 2805    C_ wss 3461   (/)c0 3783    X. cxp 4986   "cima 4991   ` cfv 5570  (class class class)co 6270   0cc0 9481   RR+crp 11221   [,)cico 11534   Basecbs 14719   TopOpenctopn 14914   *Metcxmt 18601   Metcme 18602   fBascfbas 18604   MetOpencmopn 18606  metUnifOLDcmetuOLD 18607   Filcfil 20515    fLim cflim 20604  UnifOncust 20871  unifTopcutop 20902  UnifStcuss 20925  UnifSpcusp 20926  toUnifSpctus 20927  CauFiluccfilu 20958  CUnifSpccusp 20969  CauFilccfil 21860   CMetcms 21862
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-rep 4550  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565  ax-cnex 9537  ax-resscn 9538  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-addrcl 9542  ax-mulcl 9543  ax-mulrcl 9544  ax-mulcom 9545  ax-addass 9546  ax-mulass 9547  ax-distr 9548  ax-i2m1 9549  ax-1ne0 9550  ax-1rid 9551  ax-rnegex 9552  ax-rrecex 9553  ax-cnre 9554  ax-pre-lttri 9555  ax-pre-lttrn 9556  ax-pre-ltadd 9557  ax-pre-mulgt0 9558  ax-pre-sup 9559
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-nel 2652  df-ral 2809  df-rex 2810  df-reu 2811  df-rmo 2812  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-tp 4021  df-op 4023  df-uni 4236  df-int 4272  df-iun 4317  df-br 4440  df-opab 4498  df-mpt 4499  df-tr 4533  df-eprel 4780  df-id 4784  df-po 4789  df-so 4790  df-fr 4827  df-we 4829  df-ord 4870  df-on 4871  df-lim 4872  df-suc 4873  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578  df-riota 6232  df-ov 6273  df-oprab 6274  df-mpt2 6275  df-om 6674  df-1st 6773  df-2nd 6774  df-recs 7034  df-rdg 7068  df-1o 7122  df-oadd 7126  df-er 7303  df-map 7414  df-en 7510  df-dom 7511  df-sdom 7512  df-fin 7513  df-sup 7893  df-pnf 9619  df-mnf 9620  df-xr 9621  df-ltxr 9622  df-le 9623  df-sub 9798  df-neg 9799  df-div 10203  df-nn 10532  df-2 10590  df-3 10591  df-4 10592  df-5 10593  df-6 10594  df-7 10595  df-8 10596  df-9 10597  df-10 10598  df-n0 10792  df-z 10861  df-dec 10977  df-uz 11083  df-q 11184  df-rp 11222  df-xneg 11321  df-xadd 11322  df-xmul 11323  df-ico 11538  df-fz 11676  df-struct 14721  df-ndx 14722  df-slot 14723  df-base 14724  df-sets 14725  df-tset 14806  df-unif 14810  df-rest 14915  df-topn 14916  df-topgen 14936  df-psmet 18609  df-xmet 18610  df-met 18611  df-bl 18612  df-mopn 18613  df-fbas 18614  df-fg 18615  df-metuOLD 18616  df-fil 20516  df-ust 20872  df-utop 20903  df-uss 20928  df-usp 20929  df-tus 20930  df-cfilu 20959  df-cusp 20970  df-cfil 21863  df-cmet 21865
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator