Metamath Proof Explorer

Theorem neiflim

Description: A point is a limit point of its neighborhood filter. (Contributed by Jeff Hankins, 7-Sep-2009) (Revised by Stefan O'Rear, 9-Aug-2015)

		Ref	Expression
	Assertion	neiflim	$⊢ (J \in TopOn (X) \land A \in X) \to A \in (J fLim nei (J) (\{A\}))$

Proof

Step	Hyp	Ref	Expression
1		ssid	$⊢ nei (J) (\{A\}) \subseteq nei (J) (\{A\})$
2	1	jctr	$⊢ A \in X \to (A \in X \land nei (J) (\{A\}) \subseteq nei (J) (\{A\}))$
3	2	adantl	$⊢ (J \in TopOn (X) \land A \in X) \to (A \in X \land nei (J) (\{A\}) \subseteq nei (J) (\{A\}))$
4		simpl	$⊢ (J \in TopOn (X) \land A \in X) \to J \in TopOn (X)$
5		snssi	$⊢ A \in X \to \{A\} \subseteq X$
6	5	adantl	$⊢ (J \in TopOn (X) \land A \in X) \to \{A\} \subseteq X$
7		snnzg	$⊢ A \in X \to \{A\} \neq \emptyset$
8	7	adantl	$⊢ (J \in TopOn (X) \land A \in X) \to \{A\} \neq \emptyset$
9		neifil	$⊢ (J \in TopOn (X) \land \{A\} \subseteq X \land \{A\} \neq \emptyset) \to nei (J) (\{A\}) \in Fil (X)$
10	4 6 8 9	syl3anc	$⊢ (J \in TopOn (X) \land A \in X) \to nei (J) (\{A\}) \in Fil (X)$
11		elflim	$⊢ (J \in TopOn (X) \land nei (J) (\{A\}) \in Fil (X)) \to (A \in (J fLim nei (J) (\{A\})) \leftrightarrow (A \in X \land nei (J) (\{A\}) \subseteq nei (J) (\{A\})))$
12	10 11	syldan	$⊢ (J \in TopOn (X) \land A \in X) \to (A \in (J fLim nei (J) (\{A\})) \leftrightarrow (A \in X \land nei (J) (\{A\}) \subseteq nei (J) (\{A\})))$
13	3 12	mpbird	$⊢ (J \in TopOn (X) \land A \in X) \to A \in (J fLim nei (J) (\{A\}))$