Theorem opnneiss

Description: An open set is a neighborhood of any of its subsets. (Contributed by NM, 13-Feb-2007)

	Ref	Expression
Assertion	opnneiss	⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑁 ) → 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		simp3	⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑁 ) → 𝑆 ⊆ 𝑁 )
2		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
3	2	eltopss	⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ 𝐽 ) → 𝑁 ⊆ ∪ 𝐽 )
4		sstr	⊢ ( ( 𝑆 ⊆ 𝑁 ∧ 𝑁 ⊆ ∪ 𝐽 ) → 𝑆 ⊆ ∪ 𝐽 )
5	4	ancoms	⊢ ( ( 𝑁 ⊆ ∪ 𝐽 ∧ 𝑆 ⊆ 𝑁 ) → 𝑆 ⊆ ∪ 𝐽 )
6	3 5	stoic3	⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑁 ) → 𝑆 ⊆ ∪ 𝐽 )
7	2	opnneissb	⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ 𝐽 ∧ 𝑆 ⊆ ∪ 𝐽 ) → ( 𝑆 ⊆ 𝑁 ↔ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) )
8	6 7	syld3an3	⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑁 ) → ( 𝑆 ⊆ 𝑁 ↔ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) )
9	1 8	mpbid	⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑁 ) → 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) )