neii2

		Ref	Expression
	Assertion	neii2	$⊢ (J \in Top \land N \in nei (J) (S)) \to \exists g \in J (S \subseteq g \land g \subseteq N)$

Step	Hyp	Ref	Expression
1		eqid	$⊢ ⋃ J = ⋃ J$
2	1	neiss2	$⊢ (J \in Top \land N \in nei (J) (S)) \to S \subseteq ⋃ J$
3	1	isnei	$⊢ (J \in Top \land S \subseteq ⋃ J) \to (N \in nei (J) (S) \leftrightarrow (N \subseteq ⋃ J \land \exists g \in J (S \subseteq g \land g \subseteq N)))$
4		simpr	$⊢ (N \subseteq ⋃ J \land \exists g \in J (S \subseteq g \land g \subseteq N)) \to \exists g \in J (S \subseteq g \land g \subseteq N)$
5	3 4	biimtrdi	$⊢ (J \in Top \land S \subseteq ⋃ J) \to (N \in nei (J) (S) \to \exists g \in J (S \subseteq g \land g \subseteq N))$
6	5	impancom	$⊢ (J \in Top \land N \in nei (J) (S)) \to (S \subseteq ⋃ J \to \exists g \in J (S \subseteq g \land g \subseteq N))$
7	2 6	mpd	$⊢ (J \in Top \land N \in nei (J) (S)) \to \exists g \in J (S \subseteq g \land g \subseteq N)$

Metamath Proof Explorer