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

Metamath Proof Explorer

Theorem flimneiss

Description: A filter contains the neighborhood filter as a subfilter. (Contributed by Mario Carneiro, 9-Apr-2015) (Revised by Stefan O'Rear, 9-Aug-2015)

		Ref	Expression
	Assertion	flimneiss	$⊢ A \in (J fLim F) \to nei (J) (\{A\}) \subseteq F$

Proof

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	simprbi	$⊢ A \in (J fLim F) \to (A \in ⋃ J \land nei (J) (\{A\}) \subseteq F)$
4	3	simprd	$⊢ A \in (J fLim F) \to nei (J) (\{A\}) \subseteq F$