Definition df-lm 21033

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 21030	. 2 class ~~> t
2		vj	. . 3 setvar j
3		ctop 20698	. . 3 class Top
4		vf	. . . . . . 7 setvar f
5	4	cv 1482	. . . . . 6 class f
6	2	cv 1482	. . . . . . . 8 class j
7	6	cuni 4436	. . . . . . 7 class U. j
8		cc 9934	. . . . . . 7 class CC
9		cpm 7858	. . . . . . 7 class ^pm
10	7, 8, 9	co 6650	. . . . . 6 class ( U. j ^pm CC )
11	5, 10	wcel 1990	. . . . 5 wff f e. ( U. j ^pm CC )
12		vx	. . . . . . 7 setvar x
13	12	cv 1482	. . . . . 6 class x
14	13, 7	wcel 1990	. . . . 5 wff x e. U. j
15		vu	. . . . . . . 8 setvar u
16	12, 15	wel 1991	. . . . . . 7 wff x e. u
17		vy	. . . . . . . . . 10 setvar y
18	17	cv 1482	. . . . . . . . 9 class y
19	15	cv 1482	. . . . . . . . 9 class u
20	5, 18	cres 5116	. . . . . . . . 9 class ( f |` y )
21	18, 19, 20	wf 5884	. . . . . . . 8 wff ( f |` y ) : y --> u
22		cuz 11687	. . . . . . . . 9 class ZZ>=
23	22	crn 5115	. . . . . . . 8 class ran ZZ>=
24	21, 17, 23	wrex 2913	. . . . . . 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 2912	. . . . 5 wff A. u e. j ( x e. u -> E. y e. ran ZZ>= ( f |` y ) : y --> u )
27	11, 14, 26	w3a 1037	. . . 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 4712	. . 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 4729	. 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 1483	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  21034  lmrcl  21035  lmfval  21036