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

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 ‘ 𝐽 ) ‘ 𝑆 ) )