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

Definition df-lm 16961
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 5604, 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 16958 . 2  class  ~~> t
2 vj . . 3  set  j
3 ctop 16633 . . 3  class  Top
4 vf . . . . . . 7  set  f
54cv 1624 . . . . . 6  class  f
62cv 1624 . . . . . . . 8  class  j
76cuni 3829 . . . . . . 7  class  U. j
8 cc 8737 . . . . . . 7  class  CC
9 cpm 6775 . . . . . . 7  class  ^pm
107, 8, 9co 5860 . . . . . 6  class  ( U. j  ^pm  CC )
115, 10wcel 1686 . . . . 5  wff  f  e.  ( U. j  ^pm  CC )
12 vx . . . . . . 7  set  x
1312cv 1624 . . . . . 6  class  x
1413, 7wcel 1686 . . . . 5  wff  x  e. 
U. j
15 vu . . . . . . . 8  set  u
1612, 15wel 1687 . . . . . . 7  wff  x  e.  u
17 vy . . . . . . . . . 10  set  y
1817cv 1624 . . . . . . . . 9  class  y
1915cv 1624 . . . . . . . . 9  class  u
205, 18cres 4693 . . . . . . . . 9  class  ( f  |`  y )
2118, 19, 20wf 5253 . . . . . . . 8  wff  ( f  |`  y ) : y --> u
22 cuz 10232 . . . . . . . . 9  class  ZZ>=
2322crn 4692 . . . . . . . 8  class  ran  ZZ>=
2421, 17, 23wrex 2546 . . . . . . 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 2545 . . . . 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 4078 . . 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 4079 . 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 1625 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  16962  lmrcl  16963  lmfval  16964
  Copyright terms: Public domain W3C validator