Definition df-lm 14913

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 14910	. 2 class ~~> t
2		vj	. . 3 setvar j
3		ctop 14720	. . 3 class Top
4		vf	. . . . . . 7 setvar f
5	4	cv 1396	. . . . . 6 class f
6	2	cv 1396	. . . . . . . 8 class j
7	6	cuni 3893	. . . . . . 7 class U. j
8		cc 8029	. . . . . . 7 class CC
9		cpm 6817	. . . . . . 7 class ^pm
10	7, 8, 9	co 6017	. . . . . 6 class ( U. j ^pm CC )
11	5, 10	wcel 2202	. . . . 5 wff f e. ( U. j ^pm CC )
12		vx	. . . . . . 7 setvar x
13	12	cv 1396	. . . . . 6 class x
14	13, 7	wcel 2202	. . . . 5 wff x e. U. j
15		vu	. . . . . . . 8 setvar u
16	12, 15	wel 2203	. . . . . . 7 wff x e. u
17		vy	. . . . . . . . . 10 setvar y
18	17	cv 1396	. . . . . . . . 9 class y
19	15	cv 1396	. . . . . . . . 9 class u
20	5, 18	cres 4727	. . . . . . . . 9 class ( f |` y )
21	18, 19, 20	wf 5322	. . . . . . . 8 wff ( f |` y ) : y --> u
22		cuz 9754	. . . . . . . . 9 class ZZ>=
23	22	crn 4726	. . . . . . . 8 class ran ZZ>=
24	21, 17, 23	wrex 2511	. . . . . . 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 2510	. . . . 5 wff A. u e. j ( x e. u -> E. y e. ran ZZ>= ( f |` y ) : y --> u )
27	11, 14, 26	w3a 1004	. . . 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 4149	. . 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 4150	. 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 1397	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  14914  lmrcl  14915  lmfval  14916