Definition df-cau 20772

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 20769	. 2 class Cau
2		vd	. . 3 setvar d
3		cxmt 17806	. . . . 5 class *Met
4	3	crn 4846	. . . 4 class ran *Met
5	4	cuni 4096	. . 3 class U. ran *Met
6		vj	. . . . . . . . 9 setvar j
7	6	cv 1368	. . . . . . . 8 class j
8		cuz 10866	. . . . . . . 8 class ZZ>=
9	7, 8	cfv 5423	. . . . . . 7 class ( ZZ>= ` j )
10		vf	. . . . . . . . . 10 setvar f
11	10	cv 1368	. . . . . . . . 9 class f
12	7, 11	cfv 5423	. . . . . . . 8 class ( f ` j )
13		vx	. . . . . . . . 9 setvar x
14	13	cv 1368	. . . . . . . 8 class x
15	2	cv 1368	. . . . . . . . 9 class d
16		cbl 17808	. . . . . . . . 9 class ball
17	15, 16	cfv 5423	. . . . . . . 8 class ( ball ` d )
18	12, 14, 17	co 6096	. . . . . . 7 class ( ( f ` j ) ( ball ` d ) x )
19	11, 9	cres 4847	. . . . . . 7 class ( f |` ( ZZ>= ` j ) )
20	9, 18, 19	wf 5419	. . . . . 6 wff ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( f ` j ) ( ball ` d ) x )
21		cz 10651	. . . . . 6 class ZZ
22	20, 6, 21	wrex 2721	. . . . 5 wff E. j e. ZZ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( f ` j ) ( ball ` d ) x )
23		crp 10996	. . . . 5 class RR+
24	22, 13, 23	wral 2720	. . . 4 wff A. x e. RR+ E. j e. ZZ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( f ` j ) ( ball ` d ) x )
25	15	cdm 4845	. . . . . 6 class dom d
26	25	cdm 4845	. . . . 5 class dom dom d
27		cc 9285	. . . . 5 class CC
28		cpm 7220	. . . . 5 class ^pm
29	26, 27, 28	co 6096	. . . 4 class ( dom dom d ^pm CC )
30	24, 10, 29	crab 2724	. . 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 4355	. 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 1369	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  20791