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	⊢ Rel ⇝

Proof

Step	Hyp	Ref	Expression
1		df-clim	⊢ ⇝ = { ⟨ 𝑓 , 𝑦 ⟩ ∣ ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝑓 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝑓 ‘ 𝑘 ) − 𝑦 ) ) < 𝑥 ) ) }
2	1	relopabiv	⊢ Rel ⇝