Definition df-hcau 24326

Description: Define the set of Cauchy sequences on a Hilbert space. See hcau 24537 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 24279	. 2 class Cauchy
2		vy	. . . . . . . . . . 11 setvar y
3	2	cv 1368	. . . . . . . . . 10 class y
4		vf	. . . . . . . . . . 11 setvar f
5	4	cv 1368	. . . . . . . . . 10 class f
6	3, 5	cfv 5413	. . . . . . . . 9 class ( f ` y )
7		vz	. . . . . . . . . . 11 setvar z
8	7	cv 1368	. . . . . . . . . 10 class z
9	8, 5	cfv 5413	. . . . . . . . 9 class ( f ` z )
10		cmv 24278	. . . . . . . . 9 class -h
11	6, 9, 10	co 6086	. . . . . . . 8 class ( ( f ` y ) -h ( f ` z ) )
12		cno 24276	. . . . . . . 8 class normh
13	11, 12	cfv 5413	. . . . . . 7 class ( normh ` ( ( f ` y ) -h ( f ` z ) ) )
14		vx	. . . . . . . 8 setvar x
15	14	cv 1368	. . . . . . 7 class x
16		clt 9410	. . . . . . 7 class <
17	13, 15, 16	wbr 4287	. . . . . 6 wff ( normh ` ( ( f ` y ) -h ( f ` z ) ) ) < x
18		cuz 10853	. . . . . . 7 class ZZ>=
19	3, 18	cfv 5413	. . . . . 6 class ( ZZ>= ` y )
20	17, 7, 19	wral 2710	. . . . 5 wff A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` y ) -h ( f ` z ) ) ) < x
21		cn 10314	. . . . 5 class NN
22	20, 2, 21	wrex 2711	. . . 4 wff E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` y ) -h ( f ` z ) ) ) < x
23		crp 10983	. . . 4 class RR+
24	22, 14, 23	wral 2710	. . 3 wff A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` y ) -h ( f ` z ) ) ) < x
25		chil 24272	. . . 4 class ~H
26		cmap 7206	. . . 4 class ^m
27	25, 21, 26	co 6086	. . 3 class ( ~H ^m NN )
28	24, 4, 27	crab 2714	. 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 1369	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  24332  hcau  24537