Theorem neii1

Description: A neighborhood is included in the topology's base set. (Contributed by NM, 12-Feb-2007)

	Ref	Expression
Hypothesis	neifval.1	⊢ 𝑋 = ∪ 𝐽
Assertion	neii1	⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑁 ⊆ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		neifval.1	⊢ 𝑋 = ∪ 𝐽
2	1	neiss2	⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑆 ⊆ 𝑋 )
3	1	isnei	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ↔ ( 𝑁 ⊆ 𝑋 ∧ ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) ) )
4		simpl	⊢ ( ( 𝑁 ⊆ 𝑋 ∧ ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) → 𝑁 ⊆ 𝑋 )
5	3 4	syl6bi	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) → 𝑁 ⊆ 𝑋 ) )
6	5	impancom	⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → ( 𝑆 ⊆ 𝑋 → 𝑁 ⊆ 𝑋 ) )
7	2 6	mpd	⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑁 ⊆ 𝑋 )