Metamath Proof Explorer

Theorem caufval

Description: The set of Cauchy sequences on a metric space. (Contributed by NM, 8-Sep-2006) (Revised by Mario Carneiro, 5-Sep-2015)

Ref Expression
Assertion 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 ) } )

Proof

Step Hyp Ref Expression
1 df-cau 
 |-  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 ) } )
2 dmeq 
 |-  ( d = D -> dom d = dom D )
3 2 dmeqd 
 |-  ( d = D -> dom dom d = dom dom D )
4 xmetf 
 |-  ( D e. ( *Met ` X ) -> D : ( X X. X ) --> RR* )
5 4 fdmd 
 |-  ( D e. ( *Met ` X ) -> dom D = ( X X. X ) )
6 5 dmeqd 
 |-  ( D e. ( *Met ` X ) -> dom dom D = dom ( X X. X ) )
7 dmxpid 
 |-  dom ( X X. X ) = X
8 6 7 eqtrdi 
 |-  ( D e. ( *Met ` X ) -> dom dom D = X )
9 3 8 sylan9eqr 
 |-  ( ( D e. ( *Met ` X ) /\ d = D ) -> dom dom d = X )
10 9 oveq1d 
 |-  ( ( D e. ( *Met ` X ) /\ d = D ) -> ( dom dom d ^pm CC ) = ( X ^pm CC ) )
11 simpr 
 |-  ( ( D e. ( *Met ` X ) /\ d = D ) -> d = D )
12 11 fveq2d 
 |-  ( ( D e. ( *Met ` X ) /\ d = D ) -> ( ball ` d ) = ( ball ` D ) )
13 12 oveqd 
 |-  ( ( D e. ( *Met ` X ) /\ d = D ) -> ( ( f ` k ) ( ball ` d ) x ) = ( ( f ` k ) ( ball ` D ) x ) )
14 13 feq3d 
 |-  ( ( 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 ) ) )
15 14 rexbidv 
 |-  ( ( 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 ) ) )
16 15 ralbidv 
 |-  ( ( 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 ) ) )
17 10 16 rabeqbidv 
 |-  ( ( 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 ) } )
18 fvssunirn 
 |-  ( *Met ` X ) C_ U. ran *Met
19 18 sseli 
 |-  ( D e. ( *Met ` X ) -> D e. U. ran *Met )
20 ovex 
 |-  ( X ^pm CC ) e. _V
21 20 rabex 
 |-  { 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
22 21 a1i 
 |-  ( 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 )
23 1 17 19 22 fvmptd2 
 |-  ( 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 ) } )