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

Definition df-lm 17298
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 5809, 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 17295 . 2  class  ~~> t
2 vj . . 3  set  j
3 ctop 16963 . . 3  class  Top
4 vf . . . . . . 7  set  f
54cv 1652 . . . . . 6  class  f
62cv 1652 . . . . . . . 8  class  j
76cuni 4017 . . . . . . 7  class  U. j
8 cc 8993 . . . . . . 7  class  CC
9 cpm 7022 . . . . . . 7  class  ^pm
107, 8, 9co 6084 . . . . . 6  class  ( U. j  ^pm  CC )
115, 10wcel 1726 . . . . 5  wff  f  e.  ( U. j  ^pm  CC )
12 vx . . . . . . 7  set  x
1312cv 1652 . . . . . 6  class  x
1413, 7wcel 1726 . . . . 5  wff  x  e. 
U. j
15 vu . . . . . . . 8  set  u
1612, 15wel 1727 . . . . . . 7  wff  x  e.  u
17 vy . . . . . . . . . 10  set  y
1817cv 1652 . . . . . . . . 9  class  y
1915cv 1652 . . . . . . . . 9  class  u
205, 18cres 4883 . . . . . . . . 9  class  ( f  |`  y )
2118, 19, 20wf 5453 . . . . . . . 8  wff  ( f  |`  y ) : y --> u
22 cuz 10493 . . . . . . . . 9  class  ZZ>=
2322crn 4882 . . . . . . . 8  class  ran  ZZ>=
2421, 17, 23wrex 2708 . . . . . . 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 2707 . . . . 5  wff  A. u  e.  j  ( x  e.  u  ->  E. y  e.  ran  ZZ>= ( f  |`  y ) : y --> u )
2711, 14, 26w3a 937 . . . 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 4268 . . 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 4269 . 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 1653 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  17299  lmrcl  17300  lmfval  17301
  Copyright terms: Public domain W3C validator