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	$$⊢\mathrm{Rel}\underset{t}{⇝}\left(J\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-lm	$$⊢\underset{t}{⇝}=\left(j\in \mathrm{Top}⟼\left\{⟨f,x⟩|\left(f\in \left(\bigcup j{\uparrow }_{𝑝𝑚}ℂ\right)\wedge x\in \bigcup j\wedge \forall u\in j\left(x\in u\to \exists y\in \mathrm{ran}{\mathbb{Z}}_{\ge }\left({f\upharpoonright }_y\right):y⟶u\right)\right)\right\}\right)$$
2	1	relmptopab	$$⊢\mathrm{Rel}\underset{t}{⇝}\left(J\right)$$