This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-cau

Description: Define the set of Cauchy sequences on a given extended metric space. (Contributed by NM, 8-Sep-2006)

Ref Expression
Assertion df-cau 
|- Cau = ( d e. U. ran *Met |-> { f e. ( dom dom d ^pm CC ) | A. x e. RR+ E. j e. ZZ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( f ` j ) ( ball ` d ) x ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccau 
 |-  Cau
1 vd 
 |-  d
2 cxmet 
 |-  *Met
3 2 crn 
 |-  ran *Met
4 3 cuni 
 |-  U. ran *Met
5 vf 
 |-  f
6 1 cv 
 |-  d
7 6 cdm 
 |-  dom d
8 7 cdm 
 |-  dom dom d
9 cpm 
 |-  ^pm
10 cc 
 |-  CC
11 8 10 9 co 
 |-  ( dom dom d ^pm CC )
12 vx 
 |-  x
13 crp 
 |-  RR+
14 vj 
 |-  j
15 cz 
 |-  ZZ
16 5 cv 
 |-  f
17 cuz 
 |-  ZZ>=
18 14 cv 
 |-  j
19 18 17 cfv 
 |-  ( ZZ>= ` j )
20 16 19 cres 
 |-  ( f |` ( ZZ>= ` j ) )
21 18 16 cfv 
 |-  ( f ` j )
22 cbl 
 |-  ball
23 6 22 cfv 
 |-  ( ball ` d )
24 12 cv 
 |-  x
25 21 24 23 co 
 |-  ( ( f ` j ) ( ball ` d ) x )
26 19 25 20 wf 
 |-  ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( f ` j ) ( ball ` d ) x )
27 26 14 15 wrex 
 |-  E. j e. ZZ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( f ` j ) ( ball ` d ) x )
28 27 12 13 wral 
 |-  A. x e. RR+ E. j e. ZZ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( f ` j ) ( ball ` d ) x )
29 28 5 11 crab 
 |-  { f e. ( dom dom d ^pm CC ) | A. x e. RR+ E. j e. ZZ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( f ` j ) ( ball ` d ) x ) }
30 1 4 29 cmpt 
 |-  ( d e. U. ran *Met |-> { f e. ( dom dom d ^pm CC ) | A. x e. RR+ E. j e. ZZ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( f ` j ) ( ball ` d ) x ) } )
31 0 30 wceq 
 |-  Cau = ( d e. U. ran *Met |-> { f e. ( dom dom d ^pm CC ) | A. x e. RR+ E. j e. ZZ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( f ` j ) ( ball ` d ) x ) } )