MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-lm Unicode version

Definition df-lm 16959
Description: Define a function on topologies whose value is the convergence relation for the space. Although  f is typically a function from upper integers to the topological space, it doesn't have to be. Unfortunately, the value of the function must exist to use fvmpt 5602, and we use the otherwise unnecessary conjunct  dom  f  C_  CC to ensure that. (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
StepHypRef Expression
1 clm 16956 . 2  class  ~~> t
2 vj . . 3  set  j
3 ctop 16631 . . 3  class  Top
4 vf . . . . . . 7  set  f
54cv 1622 . . . . . 6  class  f
62cv 1622 . . . . . . . 8  class  j
76cuni 3827 . . . . . . 7  class  U. j
8 cc 8735 . . . . . . 7  class  CC
9 cpm 6773 . . . . . . 7  class  ^pm
107, 8, 9co 5858 . . . . . 6  class  ( U. j  ^pm  CC )
115, 10wcel 1684 . . . . 5  wff  f  e.  ( U. j  ^pm  CC )
12 vx . . . . . . 7  set  x
1312cv 1622 . . . . . 6  class  x
1413, 7wcel 1684 . . . . 5  wff  x  e. 
U. j
15 vu . . . . . . . 8  set  u
1612, 15wel 1685 . . . . . . 7  wff  x  e.  u
17 vy . . . . . . . . . 10  set  y
1817cv 1622 . . . . . . . . 9  class  y
1915cv 1622 . . . . . . . . 9  class  u
205, 18cres 4691 . . . . . . . . 9  class  ( f  |`  y )
2118, 19, 20wf 5251 . . . . . . . 8  wff  ( f  |`  y ) : y --> u
22 cuz 10230 . . . . . . . . 9  class  ZZ>=
2322crn 4690 . . . . . . . 8  class  ran  ZZ>=
2421, 17, 23wrex 2544 . . . . . . 7  wff  E. y  e.  ran  ZZ>= ( f  |`  y ) : y --> u
2516, 24wi 4 . . . . . 6  wff  ( x  e.  u  ->  E. y  e.  ran  ZZ>= ( f  |`  y ) : y --> u )
2625, 15, 6wral 2543 . . . . 5  wff  A. u  e.  j  ( x  e.  u  ->  E. y  e.  ran  ZZ>= ( f  |`  y ) : y --> u )
2711, 14, 26w3a 934 . . . 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 ) )
2827, 4, 12copab 4076 . . 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 ) ) }
292, 3, 28cmpt 4077 . 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 ) ) } )
301, 29wceq 1623 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 ) ) } )
Colors of variables: wff set class
This definition is referenced by:  lmrel  16960  lmrcl  16961  lmfval  16962
  Copyright terms: Public domain W3C validator