Definition df-lm 15181

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 15178	. 2 class ~~> t
2		vj	. . 3 setvar j
3		ctop 14988	. . 3 class Top
4		vf	. . . . . . 7 setvar f
5	4	cv 1397	. . . . . 6 class f
6	2	cv 1397	. . . . . . . 8 class j
7	6	cuni 3919	. . . . . . 7 class U. j
8		cc 8141	. . . . . . 7 class CC
9		cpm 6896	. . . . . . 7 class ^pm
10	7, 8, 9	co 6058	. . . . . 6 class ( U. j ^pm CC )
11	5, 10	wcel 2205	. . . . 5 wff f e. ( U. j ^pm CC )
12		vx	. . . . . . 7 setvar x
13	12	cv 1397	. . . . . 6 class x
14	13, 7	wcel 2205	. . . . 5 wff x e. U. j
15		vu	. . . . . . . 8 setvar u
16	12, 15	wel 2206	. . . . . . 7 wff x e. u
17		vy	. . . . . . . . . 10 setvar y
18	17	cv 1397	. . . . . . . . 9 class y
19	15	cv 1397	. . . . . . . . 9 class u
20	5, 18	cres 4756	. . . . . . . . 9 class ( f |` y )
21	18, 19, 20	wf 5353	. . . . . . . 8 wff ( f |` y ) : y --> u
22		cuz 9871	. . . . . . . . 9 class ZZ>=
23	22	crn 4755	. . . . . . . 8 class ran ZZ>=
24	21, 17, 23	wrex 2523	. . . . . . 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 2522	. . . . 5 wff A. u e. j ( x e. u -> E. y e. ran ZZ>= ( f |` y ) : y --> u )
27	11, 14, 26	w3a 1005	. . . 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 4175	. . 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 4176	. 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 1398	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  15182  lmrcl  15183  lmfval  15184