This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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