Definition df-lm 15055

Description: Define a function on topologies whose value is the convergence relation for sequences into the given topological space. Although f is typically a sequence (a function from an upperset of integers) with values in the topological space, it need not be. Note, however, that the limit property concerns only values at integers, so that the real-valued function ( x e. RR |-> ( sin ` ( pi x. x ) ) ) converges to zero (in the standard topology on the reals) with this definition. (Contributed by NM, 7-Sep-2006.)

Assertion

Ref	Expression
df-lm	|- ~~> t = ( j e. Top |-> { <. f , x >. | ( f e. ( U. j ^pm CC ) /\ x e. U. j /\ A. u e. j ( x e. u -> E. y e. ran ZZ>= ( f |` y ) : y --> u ) ) } )

Distinct variable group:   f, j, x, y, u

Detailed syntax breakdown of Definition df-lm

Step	Hyp	Ref	Expression
1		clm 15052	. 2 class ~~> t
2		vj	. . 3 setvar j
3		ctop 14862	. . 3 class Top
4		vf	. . . . . . 7 setvar f
5	4	cv 1397	. . . . . 6 class f
6	2	cv 1397	. . . . . . . 8 class j
7	6	cuni 3914	. . . . . . 7 class U. j
8		cc 8125	. . . . . . 7 class CC
9		cpm 6883	. . . . . . 7 class ^pm
10	7, 8, 9	co 6050	. . . . . 6 class ( U. j ^pm CC )
11	5, 10	wcel 2203	. . . . 5 wff f e. ( U. j ^pm CC )
12		vx	. . . . . . 7 setvar x
13	12	cv 1397	. . . . . 6 class x
14	13, 7	wcel 2203	. . . . 5 wff x e. U. j
15		vu	. . . . . . . 8 setvar u
16	12, 15	wel 2204	. . . . . . 7 wff x e. u
17		vy	. . . . . . . . . 10 setvar y
18	17	cv 1397	. . . . . . . . 9 class y
19	15	cv 1397	. . . . . . . . 9 class u
20	5, 18	cres 4751	. . . . . . . . 9 class ( f |` y )
21	18, 19, 20	wf 5348	. . . . . . . 8 wff ( f |` y ) : y --> u
22		cuz 9853	. . . . . . . . 9 class ZZ>=
23	22	crn 4750	. . . . . . . 8 class ran ZZ>=
24	21, 17, 23	wrex 2521	. . . . . . 7 wff E. y e. ran ZZ>= ( f |` y ) : y --> u
25	16, 24	wi 4	. . . . . 6 wff ( x e. u -> E. y e. ran ZZ>= ( f |` y ) : y --> u )
26	25, 15, 6	wral 2520	. . . . 5 wff A. u e. j ( x e. u -> E. y e. ran ZZ>= ( f |` y ) : y --> u )
27	11, 14, 26	w3a 1005	. . . 4 wff ( f e. ( U. j ^pm CC ) /\ x e. U. j /\ A. u e. j ( x e. u -> E. y e. ran ZZ>= ( f |` y ) : y --> u ) )
28	27, 4, 12	copab 4170	. . 3 class { <. f , x >. | ( f e. ( U. j ^pm CC ) /\ x e. U. j /\ A. u e. j ( x e. u -> E. y e. ran ZZ>= ( f |` y ) : y --> u ) ) }
29	2, 3, 28	cmpt 4171	. 2 class ( j e. Top |-> { <. f , x >. | ( f e. ( U. j ^pm CC ) /\ x e. U. j /\ A. u e. j ( x e. u -> E. y e. ran ZZ>= ( f |` y ) : y --> u ) ) } )
30	1, 29	wceq 1398	1 wff ~~> t = ( j e. Top |-> { <. f , x >. | ( f e. ( U. j ^pm CC ) /\ x e. U. j /\ A. u e. j ( x e. u -> E. y e. ran ZZ>= ( f |` y ) : y --> u ) ) } )

This definition is referenced by:  lmrel  15056  lmrcl  15057  lmfval  15058