Theorem neii1

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

	Ref	Expression
Hypothesis	neifval.1	$$⊢X=\bigcup J$$
Assertion	neii1	$$⊢\left(J\in \mathrm{Top}\wedge N\in \mathrm{nei}\left(J\right)\left(S\right)\right)\to N\subseteq X$$

Proof

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