elnei

Description: A point belongs to any of its neighborhoods. Property V_iii of BourbakiTop1 p. I.3. (Contributed by FL, 28-Sep-2006)

		Ref	Expression
	Assertion	elnei	$⊢ (J \in Top \land P \in A \land N \in nei (J) (\{P\})) \to P \in N$

Step	Hyp	Ref	Expression
1		ssnei	$⊢ (J \in Top \land N \in nei (J) (\{P\})) \to \{P\} \subseteq N$
2	1	3adant2	$⊢ (J \in Top \land P \in A \land N \in nei (J) (\{P\})) \to \{P\} \subseteq N$
3		snssg	$⊢ P \in A \to (P \in N \leftrightarrow \{P\} \subseteq N)$
4	3	3ad2ant2	$⊢ (J \in Top \land P \in A \land N \in nei (J) (\{P\})) \to (P \in N \leftrightarrow \{P\} \subseteq N)$
5	2 4	mpbird	$⊢ (J \in Top \land P \in A \land N \in nei (J) (\{P\})) \to P \in N$

Metamath Proof Explorer