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

Theorem caufval 22257
Description: The set of Cauchy sequences on a metric space. (Contributed by NM, 8-Sep-2006.) (Revised by Mario Carneiro, 5-Sep-2015.)
Assertion
Ref Expression
caufval  |-  ( D  e.  ( *Met `  X )  ->  ( Cau `  D )  =  { f  e.  ( X  ^pm  CC )  |  A. x  e.  RR+  E. k  e.  ZZ  (
f  |`  ( ZZ>= `  k
) ) : (
ZZ>= `  k ) --> ( ( f `  k
) ( ball `  D
) x ) } )
Distinct variable groups:    f, k, x, D    f, X, k, x

Proof of Theorem caufval
Dummy variable  d is distinct from all other variables.
StepHypRef Expression
1 df-cau 22238 . . 3  |-  Cau  =  ( d  e.  U. ran  *Met  |->  { f  e.  ( dom  dom  d  ^pm  CC )  | 
A. x  e.  RR+  E. k  e.  ZZ  (
f  |`  ( ZZ>= `  k
) ) : (
ZZ>= `  k ) --> ( ( f `  k
) ( ball `  d
) x ) } )
21a1i 11 . 2  |-  ( D  e.  ( *Met `  X )  ->  Cau  =  ( d  e. 
U. ran  *Met  |->  { f  e.  ( dom  dom  d  ^pm  CC )  |  A. x  e.  RR+  E. k  e.  ZZ  ( f  |`  ( ZZ>= `  k )
) : ( ZZ>= `  k ) --> ( ( f `  k ) ( ball `  d
) x ) } ) )
3 dmeq 5038 . . . . . 6  |-  ( d  =  D  ->  dom  d  =  dom  D )
43dmeqd 5040 . . . . 5  |-  ( d  =  D  ->  dom  dom  d  =  dom  dom  D )
5 xmetf 21356 . . . . . . . 8  |-  ( D  e.  ( *Met `  X )  ->  D : ( X  X.  X ) --> RR* )
6 fdm 5738 . . . . . . . 8  |-  ( D : ( X  X.  X ) --> RR*  ->  dom 
D  =  ( X  X.  X ) )
75, 6syl 17 . . . . . . 7  |-  ( D  e.  ( *Met `  X )  ->  dom  D  =  ( X  X.  X ) )
87dmeqd 5040 . . . . . 6  |-  ( D  e.  ( *Met `  X )  ->  dom  dom 
D  =  dom  ( X  X.  X ) )
9 dmxpid 5057 . . . . . 6  |-  dom  ( X  X.  X )  =  X
108, 9syl6eq 2503 . . . . 5  |-  ( D  e.  ( *Met `  X )  ->  dom  dom 
D  =  X )
114, 10sylan9eqr 2509 . . . 4  |-  ( ( D  e.  ( *Met `  X )  /\  d  =  D )  ->  dom  dom  d  =  X )
1211oveq1d 6310 . . 3  |-  ( ( D  e.  ( *Met `  X )  /\  d  =  D )  ->  ( dom  dom  d  ^pm  CC )  =  ( X  ^pm  CC ) )
13 simpr 463 . . . . . . . 8  |-  ( ( D  e.  ( *Met `  X )  /\  d  =  D )  ->  d  =  D )
1413fveq2d 5874 . . . . . . 7  |-  ( ( D  e.  ( *Met `  X )  /\  d  =  D )  ->  ( ball `  d )  =  (
ball `  D )
)
1514oveqd 6312 . . . . . 6  |-  ( ( D  e.  ( *Met `  X )  /\  d  =  D )  ->  ( (
f `  k )
( ball `  d )
x )  =  ( ( f `  k
) ( ball `  D
) x ) )
1615feq3d 5721 . . . . 5  |-  ( ( D  e.  ( *Met `  X )  /\  d  =  D )  ->  ( (
f  |`  ( ZZ>= `  k
) ) : (
ZZ>= `  k ) --> ( ( f `  k
) ( ball `  d
) x )  <->  ( f  |`  ( ZZ>= `  k )
) : ( ZZ>= `  k ) --> ( ( f `  k ) ( ball `  D
) x ) ) )
1716rexbidv 2903 . . . 4  |-  ( ( D  e.  ( *Met `  X )  /\  d  =  D )  ->  ( E. k  e.  ZZ  (
f  |`  ( ZZ>= `  k
) ) : (
ZZ>= `  k ) --> ( ( f `  k
) ( ball `  d
) x )  <->  E. k  e.  ZZ  ( f  |`  ( ZZ>= `  k )
) : ( ZZ>= `  k ) --> ( ( f `  k ) ( ball `  D
) x ) ) )
1817ralbidv 2829 . . 3  |-  ( ( D  e.  ( *Met `  X )  /\  d  =  D )  ->  ( A. x  e.  RR+  E. k  e.  ZZ  ( f  |`  ( ZZ>= `  k )
) : ( ZZ>= `  k ) --> ( ( f `  k ) ( ball `  d
) x )  <->  A. x  e.  RR+  E. k  e.  ZZ  ( f  |`  ( ZZ>= `  k )
) : ( ZZ>= `  k ) --> ( ( f `  k ) ( ball `  D
) x ) ) )
1912, 18rabeqbidv 3042 . 2  |-  ( ( D  e.  ( *Met `  X )  /\  d  =  D )  ->  { f  e.  ( dom  dom  d  ^pm  CC )  |  A. x  e.  RR+  E. k  e.  ZZ  ( f  |`  ( ZZ>= `  k )
) : ( ZZ>= `  k ) --> ( ( f `  k ) ( ball `  d
) x ) }  =  { f  e.  ( X  ^pm  CC )  |  A. x  e.  RR+  E. k  e.  ZZ  ( f  |`  ( ZZ>= `  k )
) : ( ZZ>= `  k ) --> ( ( f `  k ) ( ball `  D
) x ) } )
20 fvssunirn 5893 . . 3  |-  ( *Met `  X ) 
C_  U. ran  *Met
2120sseli 3430 . 2  |-  ( D  e.  ( *Met `  X )  ->  D  e.  U. ran  *Met )
22 ovex 6323 . . . 4  |-  ( X 
^pm  CC )  e.  _V
2322rabex 4557 . . 3  |-  { f  e.  ( X  ^pm  CC )  |  A. x  e.  RR+  E. k  e.  ZZ  ( f  |`  ( ZZ>= `  k )
) : ( ZZ>= `  k ) --> ( ( f `  k ) ( ball `  D
) x ) }  e.  _V
2423a1i 11 . 2  |-  ( D  e.  ( *Met `  X )  ->  { f  e.  ( X  ^pm  CC )  |  A. x  e.  RR+  E. k  e.  ZZ  ( f  |`  ( ZZ>= `  k )
) : ( ZZ>= `  k ) --> ( ( f `  k ) ( ball `  D
) x ) }  e.  _V )
252, 19, 21, 24fvmptd 5959 1  |-  ( D  e.  ( *Met `  X )  ->  ( Cau `  D )  =  { f  e.  ( X  ^pm  CC )  |  A. x  e.  RR+  E. k  e.  ZZ  (
f  |`  ( ZZ>= `  k
) ) : (
ZZ>= `  k ) --> ( ( f `  k
) ( ball `  D
) x ) } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    = wceq 1446    e. wcel 1889   A.wral 2739   E.wrex 2740   {crab 2743   _Vcvv 3047   U.cuni 4201    |-> cmpt 4464    X. cxp 4835   dom cdm 4837   ran crn 4838    |` cres 4839   -->wf 5581   ` cfv 5585  (class class class)co 6295    ^pm cpm 7478   CCcc 9542   RR*cxr 9679   ZZcz 10944   ZZ>=cuz 11166   RR+crp 11309   *Metcxmt 18967   ballcbl 18969   Caucca 22235
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-8 1891  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-sep 4528  ax-nul 4537  ax-pow 4584  ax-pr 4642  ax-un 6588  ax-cnex 9600  ax-resscn 9601
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-eu 2305  df-mo 2306  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-ral 2744  df-rex 2745  df-rab 2748  df-v 3049  df-sbc 3270  df-csb 3366  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3734  df-if 3884  df-pw 3955  df-sn 3971  df-pr 3973  df-op 3977  df-uni 4202  df-br 4406  df-opab 4465  df-mpt 4466  df-id 4752  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-iota 5549  df-fun 5587  df-fn 5588  df-f 5589  df-fv 5593  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-map 7479  df-xr 9684  df-xmet 18975  df-cau 22238
This theorem is referenced by:  iscau  22258  equivcau  22282
  Copyright terms: Public domain W3C validator