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