Metamath Proof Explorer


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 ⇝𝑟