Metamath Proof Explorer


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 ‘ 𝐽 ) ‘ 𝑆 ) )