Metamath Proof Explorer

Theorem lmrcl

Description: Reverse closure for the convergence relation. (Contributed by Mario Carneiro, 7-Sep-2015)

Ref Expression
Assertion lmrcl ⊢ F ⇝t ⁡ J P → J ∈ Top

Proof

Step Hyp Ref Expression
1 df-lm ⊢ ⇝t = j ∈ Top ⟼ f x | f ∈ ⋃ j ↑ 𝑝𝑚 ℂ ∧ x ∈ ⋃ j ∧ ∀ u ∈ j x ∈ u → ∃ y ∈ ran ⁡ ℤ ≥ f ↾ y : y ⟶ u
2 1 dmmptss ⊢ dom ⁡ ⇝t ⊆ Top
3 df-br ⊢ F ⇝t ⁡ J P ↔ F P ∈ ⇝t ⁡ J
4 elfvdm ⊢ F P ∈ ⇝t ⁡ J → J ∈ dom ⁡ ⇝t
5 3 4 sylbi ⊢ F ⇝t ⁡ J P → J ∈ dom ⁡ ⇝t
6 2 5 sseldi ⊢ F ⇝t ⁡ J P → J ∈ Top