neii1

Description: A neighborhood is included in the topology's base set. (Contributed by NM, 12-Feb-2007)

		Ref	Expression
	Hypothesis	neifval.1	$⊢ X = ⋃ J$
	Assertion	neii1	$⊢ (J \in Top \land N \in nei (J) (S)) \to N \subseteq X$

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

Metamath Proof Explorer