opnneiid

Description: Only an open set is a neighborhood of itself. (Contributed by FL, 2-Oct-2006)

		Ref	Expression
	Assertion	opnneiid	$⊢ J \in Top \to (N \in nei (J) (N) \leftrightarrow N \in J)$

Step	Hyp	Ref	Expression
1		neii2	$⊢ (J \in Top \land N \in nei (J) (N)) \to \exists x \in J (N \subseteq x \land x \subseteq N)$
2		eqss	$⊢ N = x \leftrightarrow (N \subseteq x \land x \subseteq N)$
3		eleq1a	$⊢ x \in J \to (N = x \to N \in J)$
4	2 3	biimtrrid	$⊢ x \in J \to ((N \subseteq x \land x \subseteq N) \to N \in J)$
5	4	rexlimiv	$⊢ \exists x \in J (N \subseteq x \land x \subseteq N) \to N \in J$
6	1 5	syl	$⊢ (J \in Top \land N \in nei (J) (N)) \to N \in J$
7	6	ex	$⊢ J \in Top \to (N \in nei (J) (N) \to N \in J)$
8		ssid	$⊢ N \subseteq N$
9		opnneiss	$⊢ (J \in Top \land N \in J \land N \subseteq N) \to N \in nei (J) (N)$
10	9	3exp	$⊢ J \in Top \to (N \in J \to (N \subseteq N \to N \in nei (J) (N)))$
11	8 10	mpii	$⊢ J \in Top \to (N \in J \to N \in nei (J) (N))$
12	7 11	impbid	$⊢ J \in Top \to (N \in nei (J) (N) \leftrightarrow N \in J)$

Metamath Proof Explorer