Definition df-lm 12984

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 12981	. 2 class ~~> t
2		vj	. . 3 setvar j
3		ctop 12789	. . 3 class Top
4		vf	. . . . . . 7 setvar f
5	4	cv 1347	. . . . . 6 class f
6	2	cv 1347	. . . . . . . 8 class j
7	6	cuni 3796	. . . . . . 7 class U. j
8		cc 7772	. . . . . . 7 class CC
9		cpm 6627	. . . . . . 7 class ^pm
10	7, 8, 9	co 5853	. . . . . 6 class ( U. j ^pm CC )
11	5, 10	wcel 2141	. . . . 5 wff f e. ( U. j ^pm CC )
12		vx	. . . . . . 7 setvar x
13	12	cv 1347	. . . . . 6 class x
14	13, 7	wcel 2141	. . . . 5 wff x e. U. j
15		vu	. . . . . . . 8 setvar u
16	12, 15	wel 2142	. . . . . . 7 wff x e. u
17		vy	. . . . . . . . . 10 setvar y
18	17	cv 1347	. . . . . . . . 9 class y
19	15	cv 1347	. . . . . . . . 9 class u
20	5, 18	cres 4613	. . . . . . . . 9 class ( f |` y )
21	18, 19, 20	wf 5194	. . . . . . . 8 wff ( f |` y ) : y --> u
22		cuz 9487	. . . . . . . . 9 class ZZ>=
23	22	crn 4612	. . . . . . . 8 class ran ZZ>=
24	21, 17, 23	wrex 2449	. . . . . . 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 2448	. . . . 5 wff A. u e. j ( x e. u -> E. y e. ran ZZ>= ( f |` y ) : y --> u )
27	11, 14, 26	w3a 973	. . . 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 4049	. . 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 4050	. 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 1348	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:  lmrcl  12985  lmfval  12986