Theorem lmrel

Description: The topological space convergence relation is a relation. (Contributed by NM, 7-Dec-2006) (Revised by Mario Carneiro, 14-Nov-2013)

	Ref	Expression
Assertion	lmrel	⊢ Rel ( ⇝𝑡 ‘ 𝐽 )

Proof

Step	Hyp	Ref	Expression
1		df-lm	⊢ ⇝𝑡 = ( 𝑗 ∈ Top ↦ { ⟨ 𝑓 , 𝑥 ⟩ ∣ ( 𝑓 ∈ ( ∪ 𝑗 ↑pm ℂ ) ∧ 𝑥 ∈ ∪ 𝑗 ∧ ∀ 𝑢 ∈ 𝑗 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) } )
2	1	relmptopab	⊢ Rel ( ⇝𝑡 ‘ 𝐽 )