Definition df-cau 23054

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 23051	. 2 class Cau
2		vd	. . 3 setvar d
3		cxmt 19731	. . . . 5 class *Met
4	3	crn 5115	. . . 4 class ran *Met
5	4	cuni 4436	. . 3 class U. ran *Met
6		vj	. . . . . . . . 9 setvar j
7	6	cv 1482	. . . . . . . 8 class j
8		cuz 11687	. . . . . . . 8 class ZZ>=
9	7, 8	cfv 5888	. . . . . . 7 class ( ZZ>= ` j )
10		vf	. . . . . . . . . 10 setvar f
11	10	cv 1482	. . . . . . . . 9 class f
12	7, 11	cfv 5888	. . . . . . . 8 class ( f ` j )
13		vx	. . . . . . . . 9 setvar x
14	13	cv 1482	. . . . . . . 8 class x
15	2	cv 1482	. . . . . . . . 9 class d
16		cbl 19733	. . . . . . . . 9 class ball
17	15, 16	cfv 5888	. . . . . . . 8 class ( ball ` d )
18	12, 14, 17	co 6650	. . . . . . 7 class ( ( f ` j ) ( ball ` d ) x )
19	11, 9	cres 5116	. . . . . . 7 class ( f |` ( ZZ>= ` j ) )
20	9, 18, 19	wf 5884	. . . . . 6 wff ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( f ` j ) ( ball ` d ) x )
21		cz 11377	. . . . . 6 class ZZ
22	20, 6, 21	wrex 2913	. . . . 5 wff E. j e. ZZ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( f ` j ) ( ball ` d ) x )
23		crp 11832	. . . . 5 class RR+
24	22, 13, 23	wral 2912	. . . 4 wff A. x e. RR+ E. j e. ZZ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( f ` j ) ( ball ` d ) x )
25	15	cdm 5114	. . . . . 6 class dom d
26	25	cdm 5114	. . . . 5 class dom dom d
27		cc 9934	. . . . 5 class CC
28		cpm 7858	. . . . 5 class ^pm
29	26, 27, 28	co 6650	. . . 4 class ( dom dom d ^pm CC )
30	24, 10, 29	crab 2916	. . 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 4729	. 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 1483	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  23073