Metamath Proof Explorer


Theorem lmrel

Description: The topological space convergence relation is a relation. (Contributed by NM, 7-Dec-2006) (Revised by Mario Carneiro, 14-Nov-2013)

Ref Expression
Assertion lmrel Rel t J

Proof

Step Hyp Ref Expression
1 df-lm t = j Top f x | f j 𝑝𝑚 x j u j x u y ran f y : y u
2 1 relmptopab Rel t J