Definition df-lm 12359

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 12356	. 2 class ~~> t
2		vj	. . 3 setvar j
3		ctop 12164	. . 3 class Top
4		vf	. . . . . . 7 setvar f
5	4	cv 1330	. . . . . 6 class f
6	2	cv 1330	. . . . . . . 8 class j
7	6	cuni 3736	. . . . . . 7 class U. j
8		cc 7618	. . . . . . 7 class CC
9		cpm 6543	. . . . . . 7 class ^pm
10	7, 8, 9	co 5774	. . . . . 6 class ( U. j ^pm CC )
11	5, 10	wcel 1480	. . . . 5 wff f e. ( U. j ^pm CC )
12		vx	. . . . . . 7 setvar x
13	12	cv 1330	. . . . . 6 class x
14	13, 7	wcel 1480	. . . . 5 wff x e. U. j
15		vu	. . . . . . . 8 setvar u
16	12, 15	wel 1481	. . . . . . 7 wff x e. u
17		vy	. . . . . . . . . 10 setvar y
18	17	cv 1330	. . . . . . . . 9 class y
19	15	cv 1330	. . . . . . . . 9 class u
20	5, 18	cres 4541	. . . . . . . . 9 class ( f |` y )
21	18, 19, 20	wf 5119	. . . . . . . 8 wff ( f |` y ) : y --> u
22		cuz 9326	. . . . . . . . 9 class ZZ>=
23	22	crn 4540	. . . . . . . 8 class ran ZZ>=
24	21, 17, 23	wrex 2417	. . . . . . 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 2416	. . . . 5 wff A. u e. j ( x e. u -> E. y e. ran ZZ>= ( f |` y ) : y --> u )
27	11, 14, 26	w3a 962	. . . 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 3988	. . 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 3989	. 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 1331	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  12360  lmfval  12361