Definition df-hcau 27830

Description: Define the set of Cauchy sequences on a Hilbert space. See hcau 28041 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 27783	. 2 class Cauchy
2		vy	. . . . . . . . . . 11 setvar y
3	2	cv 1482	. . . . . . . . . 10 class y
4		vf	. . . . . . . . . . 11 setvar f
5	4	cv 1482	. . . . . . . . . 10 class f
6	3, 5	cfv 5888	. . . . . . . . 9 class ( f ` y )
7		vz	. . . . . . . . . . 11 setvar z
8	7	cv 1482	. . . . . . . . . 10 class z
9	8, 5	cfv 5888	. . . . . . . . 9 class ( f ` z )
10		cmv 27782	. . . . . . . . 9 class -h
11	6, 9, 10	co 6650	. . . . . . . 8 class ( ( f ` y ) -h ( f ` z ) )
12		cno 27780	. . . . . . . 8 class normh
13	11, 12	cfv 5888	. . . . . . 7 class ( normh ` ( ( f ` y ) -h ( f ` z ) ) )
14		vx	. . . . . . . 8 setvar x
15	14	cv 1482	. . . . . . 7 class x
16		clt 10074	. . . . . . 7 class <
17	13, 15, 16	wbr 4653	. . . . . 6 wff ( normh ` ( ( f ` y ) -h ( f ` z ) ) ) < x
18		cuz 11687	. . . . . . 7 class ZZ>=
19	3, 18	cfv 5888	. . . . . 6 class ( ZZ>= ` y )
20	17, 7, 19	wral 2912	. . . . 5 wff A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` y ) -h ( f ` z ) ) ) < x
21		cn 11020	. . . . 5 class NN
22	20, 2, 21	wrex 2913	. . . 4 wff E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` y ) -h ( f ` z ) ) ) < x
23		crp 11832	. . . 4 class RR+
24	22, 14, 23	wral 2912	. . 3 wff A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` y ) -h ( f ` z ) ) ) < x
25		chil 27776	. . . 4 class ~H
26		cmap 7857	. . . 4 class ^m
27	25, 21, 26	co 6650	. . 3 class ( ~H ^m NN )
28	24, 4, 27	crab 2916	. 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 1483	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  27836  hcau  28041