Theorem climrel

Description: The limit relation is a relation. (Contributed by NM, 28-Aug-2005) (Revised by Mario Carneiro, 31-Jan-2014)

	Ref	Expression
Assertion	climrel	$$⊢\mathrm{Rel}⇝$$

Proof

Step	Hyp	Ref	Expression
1		df-clim	$$⊢⇝=\left\{⟨f,y⟩|\left(y\in ℂ\wedge \forall x\in {ℝ}^{+}\exists j\in \mathbb{Z}\forall k\in {\mathbb{Z}}_{\ge j}\left(f\left(k\right)\in ℂ\wedge \left|f\left(k\right)-y\right|<x\right)\right)\right\}$$
2	1	relopabi	$$⊢\mathrm{Rel}⇝$$