Definition df-hcau 24198

Description: Define the set of Cauchy sequences on a Hilbert space. See hcau 24409 for its membership relation. Note that f : NN --> ~H is an infinite sequence of vectors, i.e. a mapping from integers to vectors. Definition of Cauchy sequence in [Beran] p. 96. (Contributed by NM, 6-Jun-2008.) (New usage is discouraged.)

Assertion

Ref	Expression
df-hcau	|- Cauchy = { f e. ( ~H ^m NN ) | A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` y ) -h ( f ` z ) ) ) < x }

Distinct variable group:   x, y, z, f

Detailed syntax breakdown of Definition df-hcau

Step	Hyp	Ref	Expression
1		ccau 24151	. 2 class Cauchy
2		vy	. . . . . . . . . . 11 setvar y
3	2	cv 1361	. . . . . . . . . 10 class y
4		vf	. . . . . . . . . . 11 setvar f
5	4	cv 1361	. . . . . . . . . 10 class f
6	3, 5	cfv 5406	. . . . . . . . 9 class ( f ` y )
7		vz	. . . . . . . . . . 11 setvar z
8	7	cv 1361	. . . . . . . . . 10 class z
9	8, 5	cfv 5406	. . . . . . . . 9 class ( f ` z )
10		cmv 24150	. . . . . . . . 9 class -h
11	6, 9, 10	co 6080	. . . . . . . 8 class ( ( f ` y ) -h ( f ` z ) )
12		cno 24148	. . . . . . . 8 class normh
13	11, 12	cfv 5406	. . . . . . 7 class ( normh ` ( ( f ` y ) -h ( f ` z ) ) )
14		vx	. . . . . . . 8 setvar x
15	14	cv 1361	. . . . . . 7 class x
16		clt 9406	. . . . . . 7 class <
17	13, 15, 16	wbr 4280	. . . . . 6 wff ( normh ` ( ( f ` y ) -h ( f ` z ) ) ) < x
18		cuz 10849	. . . . . . 7 class ZZ>=
19	3, 18	cfv 5406	. . . . . 6 class ( ZZ>= ` y )
20	17, 7, 19	wral 2705	. . . . 5 wff A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` y ) -h ( f ` z ) ) ) < x
21		cn 10310	. . . . 5 class NN
22	20, 2, 21	wrex 2706	. . . 4 wff E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` y ) -h ( f ` z ) ) ) < x
23		crp 10979	. . . 4 class RR+
24	22, 14, 23	wral 2705	. . 3 wff A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` y ) -h ( f ` z ) ) ) < x
25		chil 24144	. . . 4 class ~H
26		cmap 7202	. . . 4 class ^m
27	25, 21, 26	co 6080	. . 3 class ( ~H ^m NN )
28	24, 4, 27	crab 2709	. 2 class { f e. ( ~H ^m NN ) | A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` y ) -h ( f ` z ) ) ) < x }
29	1, 28	wceq 1362	1 wff Cauchy = { f e. ( ~H ^m NN ) | A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` y ) -h ( f ` z ) ) ) < x }

This definition is referenced by:  h2hcau  24204  hcau  24409