Definition df-lm 13693

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 13690	. 2 class ~~> t
2		vj	. . 3 setvar j
3		ctop 13500	. . 3 class Top
4		vf	. . . . . . 7 setvar f
5	4	cv 1352	. . . . . 6 class f
6	2	cv 1352	. . . . . . . 8 class j
7	6	cuni 3810	. . . . . . 7 class U. j
8		cc 7809	. . . . . . 7 class CC
9		cpm 6649	. . . . . . 7 class ^pm
10	7, 8, 9	co 5875	. . . . . 6 class ( U. j ^pm CC )
11	5, 10	wcel 2148	. . . . 5 wff f e. ( U. j ^pm CC )
12		vx	. . . . . . 7 setvar x
13	12	cv 1352	. . . . . 6 class x
14	13, 7	wcel 2148	. . . . 5 wff x e. U. j
15		vu	. . . . . . . 8 setvar u
16	12, 15	wel 2149	. . . . . . 7 wff x e. u
17		vy	. . . . . . . . . 10 setvar y
18	17	cv 1352	. . . . . . . . 9 class y
19	15	cv 1352	. . . . . . . . 9 class u
20	5, 18	cres 4629	. . . . . . . . 9 class ( f |` y )
21	18, 19, 20	wf 5213	. . . . . . . 8 wff ( f |` y ) : y --> u
22		cuz 9528	. . . . . . . . 9 class ZZ>=
23	22	crn 4628	. . . . . . . 8 class ran ZZ>=
24	21, 17, 23	wrex 2456	. . . . . . 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 2455	. . . . 5 wff A. u e. j ( x e. u -> E. y e. ran ZZ>= ( f |` y ) : y --> u )
27	11, 14, 26	w3a 978	. . . 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 4064	. . 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 4065	. 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 1353	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  13694  lmfval  13695