Metamath Proof Explorer


Theorem ssnei

Description: A set is included in any of its neighborhoods. Generalization to subsets of elnei . (Contributed by FL, 16-Nov-2006)

Ref Expression
Assertion ssnei ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑆𝑁 )

Proof

Step Hyp Ref Expression
1 neii2 ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → ∃ 𝑔𝐽 ( 𝑆𝑔𝑔𝑁 ) )
2 sstr ( ( 𝑆𝑔𝑔𝑁 ) → 𝑆𝑁 )
3 2 rexlimivw ( ∃ 𝑔𝐽 ( 𝑆𝑔𝑔𝑁 ) → 𝑆𝑁 )
4 1 3 syl ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑆𝑁 )