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