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 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 ) ) } )
2 1 relmptopab 
 |-  Rel ( ~~>t ` J )