This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rlimrel

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

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

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