Definition df-cau 21864

Description: Define a function on metric spaces whose value is the set of Cauchy sequences of the space. (Contributed by NM, 8-Sep-2006.)

Assertion

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

Distinct variable group:   f, d, j, x

Detailed syntax breakdown of Definition df-cau

Step	Hyp	Ref	Expression
1		cca 21861	. 2 class Cau
2		vd	. . 3 setvar d
3		cxmt 18601	. . . . 5 class *Met
4	3	crn 4989	. . . 4 class ran *Met
5	4	cuni 4235	. . 3 class U. ran *Met
6		vj	. . . . . . . . 9 setvar j
7	6	cv 1397	. . . . . . . 8 class j
8		cuz 11082	. . . . . . . 8 class ZZ>=
9	7, 8	cfv 5570	. . . . . . 7 class ( ZZ>= ` j )
10		vf	. . . . . . . . . 10 setvar f
11	10	cv 1397	. . . . . . . . 9 class f
12	7, 11	cfv 5570	. . . . . . . 8 class ( f ` j )
13		vx	. . . . . . . . 9 setvar x
14	13	cv 1397	. . . . . . . 8 class x
15	2	cv 1397	. . . . . . . . 9 class d
16		cbl 18603	. . . . . . . . 9 class ball
17	15, 16	cfv 5570	. . . . . . . 8 class ( ball ` d )
18	12, 14, 17	co 6270	. . . . . . 7 class ( ( f ` j ) ( ball ` d ) x )
19	11, 9	cres 4990	. . . . . . 7 class ( f |` ( ZZ>= ` j ) )
20	9, 18, 19	wf 5566	. . . . . 6 wff ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( f ` j ) ( ball ` d ) x )
21		cz 10860	. . . . . 6 class ZZ
22	20, 6, 21	wrex 2805	. . . . 5 wff E. j e. ZZ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( f ` j ) ( ball ` d ) x )
23		crp 11221	. . . . 5 class RR+
24	22, 13, 23	wral 2804	. . . 4 wff A. x e. RR+ E. j e. ZZ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( f ` j ) ( ball ` d ) x )
25	15	cdm 4988	. . . . . 6 class dom d
26	25	cdm 4988	. . . . 5 class dom dom d
27		cc 9479	. . . . 5 class CC
28		cpm 7413	. . . . 5 class ^pm
29	26, 27, 28	co 6270	. . . 4 class ( dom dom d ^pm CC )
30	24, 10, 29	crab 2808	. . 3 class { 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	2, 5, 30	cmpt 4497	. 2 class ( 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 ) } )
32	1, 31	wceq 1398	1 wff 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 ) } )

This definition is referenced by:  caufval  21883