Definition df-lm 12830

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 12827	. 2 class ~~> t
2		vj	. . 3 setvar j
3		ctop 12635	. . 3 class Top
4		vf	. . . . . . 7 setvar f
5	4	cv 1342	. . . . . 6 class f
6	2	cv 1342	. . . . . . . 8 class j
7	6	cuni 3789	. . . . . . 7 class U. j
8		cc 7751	. . . . . . 7 class CC
9		cpm 6615	. . . . . . 7 class ^pm
10	7, 8, 9	co 5842	. . . . . 6 class ( U. j ^pm CC )
11	5, 10	wcel 2136	. . . . 5 wff f e. ( U. j ^pm CC )
12		vx	. . . . . . 7 setvar x
13	12	cv 1342	. . . . . 6 class x
14	13, 7	wcel 2136	. . . . 5 wff x e. U. j
15		vu	. . . . . . . 8 setvar u
16	12, 15	wel 2137	. . . . . . 7 wff x e. u
17		vy	. . . . . . . . . 10 setvar y
18	17	cv 1342	. . . . . . . . 9 class y
19	15	cv 1342	. . . . . . . . 9 class u
20	5, 18	cres 4606	. . . . . . . . 9 class ( f |` y )
21	18, 19, 20	wf 5184	. . . . . . . 8 wff ( f |` y ) : y --> u
22		cuz 9466	. . . . . . . . 9 class ZZ>=
23	22	crn 4605	. . . . . . . 8 class ran ZZ>=
24	21, 17, 23	wrex 2445	. . . . . . 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 2444	. . . . 5 wff A. u e. j ( x e. u -> E. y e. ran ZZ>= ( f |` y ) : y --> u )
27	11, 14, 26	w3a 968	. . . 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 4042	. . 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 4043	. 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 1343	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  12831  lmfval  12832