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 ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑆 ⊆ 𝑁 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | neii2 | ⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) | |
2 | sstr | ⊢ ( ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) → 𝑆 ⊆ 𝑁 ) | |
3 | 2 | rexlimivw | ⊢ ( ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) → 𝑆 ⊆ 𝑁 ) |
4 | 1 3 | syl | ⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑆 ⊆ 𝑁 ) |