This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 biimtrdi ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) → ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) )
6 5 impancom ⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → ( 𝑆 ⊆ ∪ 𝐽 → ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) )
7 2 6 mpd ⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) )