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	⊢ 𝑋 = ∪ 𝐽
Assertion	tpnei	⊢ ( 𝐽 ∈ Top → ( 𝑆 ⊆ 𝑋 ↔ 𝑋 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) )

Proof

Step	Hyp	Ref	Expression
1		tpnei.1	⊢ 𝑋 = ∪ 𝐽
2	1	topopn	⊢ ( 𝐽 ∈ Top → 𝑋 ∈ 𝐽 )
3		opnneiss	⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑋 ) → 𝑋 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) )
4	3	3exp	⊢ ( 𝐽 ∈ Top → ( 𝑋 ∈ 𝐽 → ( 𝑆 ⊆ 𝑋 → 𝑋 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ) )
5	2 4	mpd	⊢ ( 𝐽 ∈ Top → ( 𝑆 ⊆ 𝑋 → 𝑋 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) )
6		ssnei	⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑆 ⊆ 𝑋 )
7	6	ex	⊢ ( 𝐽 ∈ Top → ( 𝑋 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) → 𝑆 ⊆ 𝑋 ) )
8	5 7	impbid	⊢ ( 𝐽 ∈ Top → ( 𝑆 ⊆ 𝑋 ↔ 𝑋 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) )