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

Definition df-lm 17255
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 5773, 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 17252 . 2  class  ~~> t
2 vj . . 3  set  j
3 ctop 16921 . . 3  class  Top
4 vf . . . . . . 7  set  f
54cv 1648 . . . . . 6  class  f
62cv 1648 . . . . . . . 8  class  j
76cuni 3983 . . . . . . 7  class  U. j
8 cc 8952 . . . . . . 7  class  CC
9 cpm 6986 . . . . . . 7  class  ^pm
107, 8, 9co 6048 . . . . . 6  class  ( U. j  ^pm  CC )
115, 10wcel 1721 . . . . 5  wff  f  e.  ( U. j  ^pm  CC )
12 vx . . . . . . 7  set  x
1312cv 1648 . . . . . 6  class  x
1413, 7wcel 1721 . . . . 5  wff  x  e. 
U. j
15 vu . . . . . . . 8  set  u
1612, 15wel 1722 . . . . . . 7  wff  x  e.  u
17 vy . . . . . . . . . 10  set  y
1817cv 1648 . . . . . . . . 9  class  y
1915cv 1648 . . . . . . . . 9  class  u
205, 18cres 4847 . . . . . . . . 9  class  ( f  |`  y )
2118, 19, 20wf 5417 . . . . . . . 8  wff  ( f  |`  y ) : y --> u
22 cuz 10452 . . . . . . . . 9  class  ZZ>=
2322crn 4846 . . . . . . . 8  class  ran  ZZ>=
2421, 17, 23wrex 2675 . . . . . . 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 2674 . . . . 5  wff  A. u  e.  j  ( x  e.  u  ->  E. y  e.  ran  ZZ>= ( f  |`  y ) : y --> u )
2711, 14, 26w3a 936 . . . 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 4233 . . 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 4234 . 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 1649 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  17256  lmrcl  17257  lmfval  17258
  Copyright terms: Public domain W3C validator