This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem flimtop

Description: Reverse closure for the limit point predicate. (Contributed by Mario Carneiro, 9-Apr-2015) (Revised by Stefan O'Rear, 9-Aug-2015)

		Ref	Expression
	Assertion	flimtop	$⊢ A \in (J fLim F) \to J \in Top$

Step	Hyp	Ref	Expression
1		eqid	$⊢ ⋃ J = ⋃ J$
2	1	elflim2	$⊢ A \in (J fLim F) \leftrightarrow ((J \in Top \land F \in ⋃ ran Fil \land F \subseteq 𝒫 ⋃ J) \land (A \in ⋃ J \land nei (J) (\{A\}) \subseteq F))$
3	2	simplbi	$⊢ A \in (J fLim F) \to (J \in Top \land F \in ⋃ ran Fil \land F \subseteq 𝒫 ⋃ J)$
4	3	simp1d	$⊢ A \in (J fLim F) \to J \in Top$