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

Definition df-lm 17285
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 5798, 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 17282 . 2  class  ~~> t
2 vj . . 3  set  j
3 ctop 16950 . . 3  class  Top
4 vf . . . . . . 7  set  f
54cv 1651 . . . . . 6  class  f
62cv 1651 . . . . . . . 8  class  j
76cuni 4007 . . . . . . 7  class  U. j
8 cc 8980 . . . . . . 7  class  CC
9 cpm 7011 . . . . . . 7  class  ^pm
107, 8, 9co 6073 . . . . . 6  class  ( U. j  ^pm  CC )
115, 10wcel 1725 . . . . 5  wff  f  e.  ( U. j  ^pm  CC )
12 vx . . . . . . 7  set  x
1312cv 1651 . . . . . 6  class  x
1413, 7wcel 1725 . . . . 5  wff  x  e. 
U. j
15 vu . . . . . . . 8  set  u
1612, 15wel 1726 . . . . . . 7  wff  x  e.  u
17 vy . . . . . . . . . 10  set  y
1817cv 1651 . . . . . . . . 9  class  y
1915cv 1651 . . . . . . . . 9  class  u
205, 18cres 4872 . . . . . . . . 9  class  ( f  |`  y )
2118, 19, 20wf 5442 . . . . . . . 8  wff  ( f  |`  y ) : y --> u
22 cuz 10480 . . . . . . . . 9  class  ZZ>=
2322crn 4871 . . . . . . . 8  class  ran  ZZ>=
2421, 17, 23wrex 2698 . . . . . . 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 2697 . . . . 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 4257 . . 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 4258 . 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 1652 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  17286  lmrcl  17287  lmfval  17288
  Copyright terms: Public domain W3C validator