Definition df-hcau 25566

Description: Define the set of Cauchy sequences on a Hilbert space. See hcau 25777 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 25519	. 2 class Cauchy
2		vy	. . . . . . . . . . 11 setvar y
3	2	cv 1378	. . . . . . . . . 10 class y
4		vf	. . . . . . . . . . 11 setvar f
5	4	cv 1378	. . . . . . . . . 10 class f
6	3, 5	cfv 5586	. . . . . . . . 9 class ( f ` y )
7		vz	. . . . . . . . . . 11 setvar z
8	7	cv 1378	. . . . . . . . . 10 class z
9	8, 5	cfv 5586	. . . . . . . . 9 class ( f ` z )
10		cmv 25518	. . . . . . . . 9 class -h
11	6, 9, 10	co 6282	. . . . . . . 8 class ( ( f ` y ) -h ( f ` z ) )
12		cno 25516	. . . . . . . 8 class normh
13	11, 12	cfv 5586	. . . . . . 7 class ( normh ` ( ( f ` y ) -h ( f ` z ) ) )
14		vx	. . . . . . . 8 setvar x
15	14	cv 1378	. . . . . . 7 class x
16		clt 9624	. . . . . . 7 class <
17	13, 15, 16	wbr 4447	. . . . . 6 wff ( normh ` ( ( f ` y ) -h ( f ` z ) ) ) < x
18		cuz 11078	. . . . . . 7 class ZZ>=
19	3, 18	cfv 5586	. . . . . 6 class ( ZZ>= ` y )
20	17, 7, 19	wral 2814	. . . . 5 wff A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` y ) -h ( f ` z ) ) ) < x
21		cn 10532	. . . . 5 class NN
22	20, 2, 21	wrex 2815	. . . 4 wff E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` y ) -h ( f ` z ) ) ) < x
23		crp 11216	. . . 4 class RR+
24	22, 14, 23	wral 2814	. . 3 wff A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` y ) -h ( f ` z ) ) ) < x
25		chil 25512	. . . 4 class ~H
26		cmap 7417	. . . 4 class ^m
27	25, 21, 26	co 6282	. . 3 class ( ~H ^m NN )
28	24, 4, 27	crab 2818	. 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 1379	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  25572  hcau  25777