Definition df-cau 19162

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 19159	. 2 class Cau
2		vd	. . 3 set d
3		cxmt 16641	. . . . 5 class * Met
4	3	crn 4838	. . . 4 class ran * Met
5	4	cuni 3975	. . 3 class U. ran * Met
6		vj	. . . . . . . . 9 set j
7	6	cv 1648	. . . . . . . 8 class j
8		cuz 10444	. . . . . . . 8 class ZZ>=
9	7, 8	cfv 5413	. . . . . . 7 class ( ZZ>= ` j )
10		vf	. . . . . . . . . 10 set f
11	10	cv 1648	. . . . . . . . 9 class f
12	7, 11	cfv 5413	. . . . . . . 8 class ( f ` j )
13		vx	. . . . . . . . 9 set x
14	13	cv 1648	. . . . . . . 8 class x
15	2	cv 1648	. . . . . . . . 9 class d
16		cbl 16643	. . . . . . . . 9 class ball
17	15, 16	cfv 5413	. . . . . . . 8 class ( ball ` d )
18	12, 14, 17	co 6040	. . . . . . 7 class ( ( f ` j ) ( ball ` d ) x )
19	11, 9	cres 4839	. . . . . . 7 class ( f |` ( ZZ>= ` j ) )
20	9, 18, 19	wf 5409	. . . . . 6 wff ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( f ` j ) ( ball ` d ) x )
21		cz 10238	. . . . . 6 class ZZ
22	20, 6, 21	wrex 2667	. . . . 5 wff E. j e. ZZ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( f ` j ) ( ball ` d ) x )
23		crp 10568	. . . . 5 class RR+
24	22, 13, 23	wral 2666	. . . 4 wff A. x e. RR+ E. j e. ZZ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( f ` j ) ( ball ` d ) x )
25	15	cdm 4837	. . . . . 6 class dom d
26	25	cdm 4837	. . . . 5 class dom dom d
27		cc 8944	. . . . 5 class CC
28		cpm 6978	. . . . 5 class ^pm
29	26, 27, 28	co 6040	. . . 4 class ( dom dom d ^pm CC )
30	24, 10, 29	crab 2670	. . 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 4226	. 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 1649	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  19181