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