Definition df-lm 15214

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 15211	. 2 class ~~> t
2		vj	. . 3 setvar j
3		ctop 15021	. . 3 class Top
4		vf	. . . . . . 7 setvar f
5	4	cv 1401	. . . . . 6 class f
6	2	cv 1401	. . . . . . . 8 class j
7	6	cuni 3930	. . . . . . 7 class U. j
8		cc 8167	. . . . . . 7 class CC
9		cpm 6913	. . . . . . 7 class ^pm
10	7, 8, 9	co 6075	. . . . . 6 class ( U. j ^pm CC )
11	5, 10	wcel 2209	. . . . 5 wff f e. ( U. j ^pm CC )
12		vx	. . . . . . 7 setvar x
13	12	cv 1401	. . . . . 6 class x
14	13, 7	wcel 2209	. . . . 5 wff x e. U. j
15		vu	. . . . . . . 8 setvar u
16	12, 15	wel 2210	. . . . . . 7 wff x e. u
17		vy	. . . . . . . . . 10 setvar y
18	17	cv 1401	. . . . . . . . 9 class y
19	15	cv 1401	. . . . . . . . 9 class u
20	5, 18	cres 4771	. . . . . . . . 9 class ( f |` y )
21	18, 19, 20	wf 5368	. . . . . . . 8 wff ( f |` y ) : y --> u
22		cuz 9900	. . . . . . . . 9 class ZZ>=
23	22	crn 4770	. . . . . . . 8 class ran ZZ>=
24	21, 17, 23	wrex 2529	. . . . . . 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 2528	. . . . 5 wff A. u e. j ( x e. u -> E. y e. ran ZZ>= ( f |` y ) : y --> u )
27	11, 14, 26	w3a 1009	. . . 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 4186	. . 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 4187	. 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 1402	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  15215  lmrcl  15216  lmfval  15217