Theorem rlimrel

Description: The limit relation is a relation. (Contributed by Mario Carneiro, 24-Sep-2014)

	Ref	Expression
Assertion	rlimrel	$$⊢\mathrm{Rel}\underset{ℝ}{⇝}$$

Proof

Step	Hyp	Ref	Expression
1		df-rlim	$$⊢\underset{ℝ}{⇝}=\left\{⟨f,x⟩|\left(\left(f\in \left(ℂ{\uparrow }_{𝑝𝑚}ℝ\right)\wedge x\in ℂ\right)\wedge \forall y\in {ℝ}^{+}\exists z\in ℝ\forall w\in \mathrm{dom}f\left(z\le w\to \left|f\left(w\right)-x\right|<y\right)\right)\right\}$$
2	1	relopabiv	$$⊢\mathrm{Rel}\underset{ℝ}{⇝}$$