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

Metamath Proof Explorer

Theorem neiss

Description: Any neighborhood of a set S is also a neighborhood of any subset R C_ S . Similar to Proposition 1 of BourbakiTop1 p. I.2. (Contributed by FL, 25-Sep-2006)

Ref Expression
Assertion neiss ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑅 ⊆ 𝑆 ) → 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
2 1 neii1 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑁 ⊆ ∪ 𝐽 )
3 2 3adant3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑅 ⊆ 𝑆 ) → 𝑁 ⊆ ∪ 𝐽 )
4 neii2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) )
5 4 3adant3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑅 ⊆ 𝑆 ) → ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) )
6 sstr2 ⊢ ( 𝑅 ⊆ 𝑆 → ( 𝑆 ⊆ 𝑔 → 𝑅 ⊆ 𝑔 ) )
7 6 anim1d ⊢ ( 𝑅 ⊆ 𝑆 → ( ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) → ( 𝑅 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) )
8 7 reximdv ⊢ ( 𝑅 ⊆ 𝑆 → ( ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) → ∃ 𝑔 ∈ 𝐽 ( 𝑅 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) )
9 8 3ad2ant3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑅 ⊆ 𝑆 ) → ( ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) → ∃ 𝑔 ∈ 𝐽 ( 𝑅 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) )
10 5 9 mpd ⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑅 ⊆ 𝑆 ) → ∃ 𝑔 ∈ 𝐽 ( 𝑅 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) )
11 simp1 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑅 ⊆ 𝑆 ) → 𝐽 ∈ Top )
12 simp3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑅 ⊆ 𝑆 ) → 𝑅 ⊆ 𝑆 )
13 1 neiss2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑆 ⊆ ∪ 𝐽 )
14 13 3adant3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑅 ⊆ 𝑆 ) → 𝑆 ⊆ ∪ 𝐽 )
15 12 14 sstrd ⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑅 ⊆ 𝑆 ) → 𝑅 ⊆ ∪ 𝐽 )
16 1 isnei ⊢ ( ( 𝐽 ∈ Top ∧ 𝑅 ⊆ ∪ 𝐽 ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑅 ) ↔ ( 𝑁 ⊆ ∪ 𝐽 ∧ ∃ 𝑔 ∈ 𝐽 ( 𝑅 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) ) )
17 11 15 16 syl2anc ⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑅 ⊆ 𝑆 ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑅 ) ↔ ( 𝑁 ⊆ ∪ 𝐽 ∧ ∃ 𝑔 ∈ 𝐽 ( 𝑅 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) ) )
18 3 10 17 mpbir2and ⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑅 ⊆ 𝑆 ) → 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑅 ) )