Definition df-lm 14662

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 14659	. 2 class ~~> t
2		vj	. . 3 setvar j
3		ctop 14469	. . 3 class Top
4		vf	. . . . . . 7 setvar f
5	4	cv 1372	. . . . . 6 class f
6	2	cv 1372	. . . . . . . 8 class j
7	6	cuni 3850	. . . . . . 7 class U. j
8		cc 7923	. . . . . . 7 class CC
9		cpm 6736	. . . . . . 7 class ^pm
10	7, 8, 9	co 5944	. . . . . 6 class ( U. j ^pm CC )
11	5, 10	wcel 2176	. . . . 5 wff f e. ( U. j ^pm CC )
12		vx	. . . . . . 7 setvar x
13	12	cv 1372	. . . . . 6 class x
14	13, 7	wcel 2176	. . . . 5 wff x e. U. j
15		vu	. . . . . . . 8 setvar u
16	12, 15	wel 2177	. . . . . . 7 wff x e. u
17		vy	. . . . . . . . . 10 setvar y
18	17	cv 1372	. . . . . . . . 9 class y
19	15	cv 1372	. . . . . . . . 9 class u
20	5, 18	cres 4677	. . . . . . . . 9 class ( f |` y )
21	18, 19, 20	wf 5267	. . . . . . . 8 wff ( f |` y ) : y --> u
22		cuz 9648	. . . . . . . . 9 class ZZ>=
23	22	crn 4676	. . . . . . . 8 class ran ZZ>=
24	21, 17, 23	wrex 2485	. . . . . . 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 2484	. . . . 5 wff A. u e. j ( x e. u -> E. y e. ran ZZ>= ( f |` y ) : y --> u )
27	11, 14, 26	w3a 981	. . . 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 4104	. . 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 4105	. 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 1373	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  14663  lmfval  14664