Theorem tpnei

Description: The underlying set of a topology is a neighborhood of any of its subsets. Special case of opnneiss . (Contributed by FL, 2-Oct-2006)

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

Proof

Step	Hyp	Ref	Expression
1		tpnei.1	$$⊢X=\bigcup J$$
2	1	topopn	$$⊢J\in \mathrm{Top}\to X\in J$$
3		opnneiss	$$⊢\left(J\in \mathrm{Top}\wedge X\in J\wedge S\subseteq X\right)\to X\in \mathrm{nei}\left(J\right)\left(S\right)$$
4	3	3exp	$$⊢J\in \mathrm{Top}\to \left(X\in J\to \left(S\subseteq X\to X\in \mathrm{nei}\left(J\right)\left(S\right)\right)\right)$$
5	2 4	mpd	$$⊢J\in \mathrm{Top}\to \left(S\subseteq X\to X\in \mathrm{nei}\left(J\right)\left(S\right)\right)$$
6		ssnei	$$⊢\left(J\in \mathrm{Top}\wedge X\in \mathrm{nei}\left(J\right)\left(S\right)\right)\to S\subseteq X$$
7	6	ex	$$⊢J\in \mathrm{Top}\to \left(X\in \mathrm{nei}\left(J\right)\left(S\right)\to S\subseteq X\right)$$
8	5 7	impbid	$$⊢J\in \mathrm{Top}\to \left(S\subseteq X\leftrightarrow X\in \mathrm{nei}\left(J\right)\left(S\right)\right)$$