Theorem rlimrel

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

	Ref	Expression
Assertion	rlimrel	⊢ Rel ⇝𝑟

Proof

Step	Hyp	Ref	Expression
1		df-rlim	⊢ ⇝𝑟 = { ⟨ 𝑓 , 𝑥 ⟩ ∣ ( ( 𝑓 ∈ ( ℂ ↑pm ℝ ) ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ dom 𝑓 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝑓 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) }
2	1	relopabiv	⊢ Rel ⇝𝑟