Definition df-lm 14904

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 14901	. 2 class ~~> t
2		vj	. . 3 setvar j
3		ctop 14711	. . 3 class Top
4		vf	. . . . . . 7 setvar f
5	4	cv 1394	. . . . . 6 class f
6	2	cv 1394	. . . . . . . 8 class j
7	6	cuni 3891	. . . . . . 7 class U. j
8		cc 8020	. . . . . . 7 class CC
9		cpm 6813	. . . . . . 7 class ^pm
10	7, 8, 9	co 6013	. . . . . 6 class ( U. j ^pm CC )
11	5, 10	wcel 2200	. . . . 5 wff f e. ( U. j ^pm CC )
12		vx	. . . . . . 7 setvar x
13	12	cv 1394	. . . . . 6 class x
14	13, 7	wcel 2200	. . . . 5 wff x e. U. j
15		vu	. . . . . . . 8 setvar u
16	12, 15	wel 2201	. . . . . . 7 wff x e. u
17		vy	. . . . . . . . . 10 setvar y
18	17	cv 1394	. . . . . . . . 9 class y
19	15	cv 1394	. . . . . . . . 9 class u
20	5, 18	cres 4725	. . . . . . . . 9 class ( f |` y )
21	18, 19, 20	wf 5320	. . . . . . . 8 wff ( f |` y ) : y --> u
22		cuz 9745	. . . . . . . . 9 class ZZ>=
23	22	crn 4724	. . . . . . . 8 class ran ZZ>=
24	21, 17, 23	wrex 2509	. . . . . . 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 2508	. . . . 5 wff A. u e. j ( x e. u -> E. y e. ran ZZ>= ( f |` y ) : y --> u )
27	11, 14, 26	w3a 1002	. . . 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 4147	. . 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 4148	. 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 1395	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  14905  lmrcl  14906  lmfval  14907