Definition df-hlim 27829

Description: Define the limit relation for Hilbert space. See hlimi 28045 for its relational expression. Note that f : NN --> ~H is an infinite sequence of vectors, i.e. a mapping from integers to vectors. Definition of converge in [Beran] p. 96. (Contributed by NM, 6-Jun-2008.) (New usage is discouraged.)

Assertion

Ref	Expression
df-hlim	|- ~~>v = { <. f , w >. | ( ( f : NN --> ~H /\ w e. ~H ) /\ A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` z ) -h w ) ) < x ) }

Distinct variable group:   x, y, z, f, w

Detailed syntax breakdown of Definition df-hlim

Step	Hyp	Ref	Expression
1		chli 27784	. 2 class ~~>v
2		cn 11020	. . . . . 6 class NN
3		chil 27776	. . . . . 6 class ~H
4		vf	. . . . . . 7 setvar f
5	4	cv 1482	. . . . . 6 class f
6	2, 3, 5	wf 5884	. . . . 5 wff f : NN --> ~H
7		vw	. . . . . . 7 setvar w
8	7	cv 1482	. . . . . 6 class w
9	8, 3	wcel 1990	. . . . 5 wff w e. ~H
10	6, 9	wa 384	. . . 4 wff ( f : NN --> ~H /\ w e. ~H )
11		vz	. . . . . . . . . . . 12 setvar z
12	11	cv 1482	. . . . . . . . . . 11 class z
13	12, 5	cfv 5888	. . . . . . . . . 10 class ( f ` z )
14		cmv 27782	. . . . . . . . . 10 class -h
15	13, 8, 14	co 6650	. . . . . . . . 9 class ( ( f ` z ) -h w )
16		cno 27780	. . . . . . . . 9 class normh
17	15, 16	cfv 5888	. . . . . . . 8 class ( normh ` ( ( f ` z ) -h w ) )
18		vx	. . . . . . . . 9 setvar x
19	18	cv 1482	. . . . . . . 8 class x
20		clt 10074	. . . . . . . 8 class <
21	17, 19, 20	wbr 4653	. . . . . . 7 wff ( normh ` ( ( f ` z ) -h w ) ) < x
22		vy	. . . . . . . . 9 setvar y
23	22	cv 1482	. . . . . . . 8 class y
24		cuz 11687	. . . . . . . 8 class ZZ>=
25	23, 24	cfv 5888	. . . . . . 7 class ( ZZ>= ` y )
26	21, 11, 25	wral 2912	. . . . . 6 wff A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` z ) -h w ) ) < x
27	26, 22, 2	wrex 2913	. . . . 5 wff E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` z ) -h w ) ) < x
28		crp 11832	. . . . 5 class RR+
29	27, 18, 28	wral 2912	. . . 4 wff A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` z ) -h w ) ) < x
30	10, 29	wa 384	. . 3 wff ( ( f : NN --> ~H /\ w e. ~H ) /\ A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` z ) -h w ) ) < x )
31	30, 4, 7	copab 4712	. 2 class { <. f , w >. | ( ( f : NN --> ~H /\ w e. ~H ) /\ A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` z ) -h w ) ) < x ) }
32	1, 31	wceq 1483	1 wff ~~>v = { <. f , w >. | ( ( f : NN --> ~H /\ w e. ~H ) /\ A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` z ) -h w ) ) < x ) }

This definition is referenced by:  h2hlm  27837  hlimi  28045