Theorem neii2

Description: Property of a neighborhood. (Contributed by NM, 12-Feb-2007)

	Ref	Expression
Assertion	neii2	⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) )

Proof

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