Definition df-cau 22119

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 22116	. 2 class Cau
2		vd	. . 3 setvar d
3		cxmt 18890	. . . . 5 class *Met
4	3	crn 4855	. . . 4 class ran *Met
5	4	cuni 4222	. . 3 class U. ran *Met
6		vj	. . . . . . . . 9 setvar j
7	6	cv 1436	. . . . . . . 8 class j
8		cuz 11159	. . . . . . . 8 class ZZ>=
9	7, 8	cfv 5601	. . . . . . 7 class ( ZZ>= ` j )
10		vf	. . . . . . . . . 10 setvar f
11	10	cv 1436	. . . . . . . . 9 class f
12	7, 11	cfv 5601	. . . . . . . 8 class ( f ` j )
13		vx	. . . . . . . . 9 setvar x
14	13	cv 1436	. . . . . . . 8 class x
15	2	cv 1436	. . . . . . . . 9 class d
16		cbl 18892	. . . . . . . . 9 class ball
17	15, 16	cfv 5601	. . . . . . . 8 class ( ball ` d )
18	12, 14, 17	co 6305	. . . . . . 7 class ( ( f ` j ) ( ball ` d ) x )
19	11, 9	cres 4856	. . . . . . 7 class ( f |` ( ZZ>= ` j ) )
20	9, 18, 19	wf 5597	. . . . . 6 wff ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( f ` j ) ( ball ` d ) x )
21		cz 10937	. . . . . 6 class ZZ
22	20, 6, 21	wrex 2783	. . . . 5 wff E. j e. ZZ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( f ` j ) ( ball ` d ) x )
23		crp 11302	. . . . 5 class RR+
24	22, 13, 23	wral 2782	. . . 4 wff A. x e. RR+ E. j e. ZZ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( f ` j ) ( ball ` d ) x )
25	15	cdm 4854	. . . . . 6 class dom d
26	25	cdm 4854	. . . . 5 class dom dom d
27		cc 9536	. . . . 5 class CC
28		cpm 7481	. . . . 5 class ^pm
29	26, 27, 28	co 6305	. . . 4 class ( dom dom d ^pm CC )
30	24, 10, 29	crab 2786	. . 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 4484	. 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 1437	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  22138