Metamath Proof Explorer


Theorem ssnei2

Description: Any subset M of X containing a neighborhood N of a set S is a neighborhood of this set. Generalization to subsets of Property V_i of BourbakiTop1 p. I.3. (Contributed by FL, 2-Oct-2006)

Ref Expression
Hypothesis neips.1 𝑋 = 𝐽
Assertion ssnei2 ( ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑁𝑀𝑀𝑋 ) ) → 𝑀 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 neips.1 𝑋 = 𝐽
2 simprr ( ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑁𝑀𝑀𝑋 ) ) → 𝑀𝑋 )
3 neii2 ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → ∃ 𝑔𝐽 ( 𝑆𝑔𝑔𝑁 ) )
4 sstr2 ( 𝑔𝑁 → ( 𝑁𝑀𝑔𝑀 ) )
5 4 com12 ( 𝑁𝑀 → ( 𝑔𝑁𝑔𝑀 ) )
6 5 anim2d ( 𝑁𝑀 → ( ( 𝑆𝑔𝑔𝑁 ) → ( 𝑆𝑔𝑔𝑀 ) ) )
7 6 reximdv ( 𝑁𝑀 → ( ∃ 𝑔𝐽 ( 𝑆𝑔𝑔𝑁 ) → ∃ 𝑔𝐽 ( 𝑆𝑔𝑔𝑀 ) ) )
8 3 7 mpan9 ( ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑁𝑀 ) → ∃ 𝑔𝐽 ( 𝑆𝑔𝑔𝑀 ) )
9 8 adantrr ( ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑁𝑀𝑀𝑋 ) ) → ∃ 𝑔𝐽 ( 𝑆𝑔𝑔𝑀 ) )
10 1 neiss2 ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑆𝑋 )
11 1 isnei ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( 𝑀 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ↔ ( 𝑀𝑋 ∧ ∃ 𝑔𝐽 ( 𝑆𝑔𝑔𝑀 ) ) ) )
12 10 11 syldan ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → ( 𝑀 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ↔ ( 𝑀𝑋 ∧ ∃ 𝑔𝐽 ( 𝑆𝑔𝑔𝑀 ) ) ) )
13 12 adantr ( ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑁𝑀𝑀𝑋 ) ) → ( 𝑀 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ↔ ( 𝑀𝑋 ∧ ∃ 𝑔𝐽 ( 𝑆𝑔𝑔𝑀 ) ) ) )
14 2 9 13 mpbir2and ( ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑁𝑀𝑀𝑋 ) ) → 𝑀 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) )