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

Definition df-lm 17247
 Description: Define a function on topologies whose value is the convergence relation for the space. Although 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 5765, and we use the otherwise unnecessary conjunct to ensure that. (Contributed by NM, 7-Sep-2006.)
Assertion
Ref Expression
df-lm
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-lm
StepHypRef Expression
1 clm 17244 . 2
2 vj . . 3
3 ctop 16913 . . 3
4 vf . . . . . . 7
54cv 1648 . . . . . 6
62cv 1648 . . . . . . . 8
76cuni 3975 . . . . . . 7
8 cc 8944 . . . . . . 7
9 cpm 6978 . . . . . . 7
107, 8, 9co 6040 . . . . . 6
115, 10wcel 1721 . . . . 5
12 vx . . . . . . 7
1312cv 1648 . . . . . 6
1413, 7wcel 1721 . . . . 5
15 vu . . . . . . . 8
1612, 15wel 1722 . . . . . . 7
17 vy . . . . . . . . . 10
1817cv 1648 . . . . . . . . 9
1915cv 1648 . . . . . . . . 9
205, 18cres 4839 . . . . . . . . 9
2118, 19, 20wf 5409 . . . . . . . 8
22 cuz 10444 . . . . . . . . 9
2322crn 4838 . . . . . . . 8
2421, 17, 23wrex 2667 . . . . . . 7
2516, 24wi 4 . . . . . 6
2625, 15, 6wral 2666 . . . . 5
2711, 14, 26w3a 936 . . . 4
2827, 4, 12copab 4225 . . 3
292, 3, 28cmpt 4226 . 2
301, 29wceq 1649 1
 Colors of variables: wff set class This definition is referenced by:  lmrel  17248  lmrcl  17249  lmfval  17250
 Copyright terms: Public domain W3C validator