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 ⊢ J ∈ Top ∧ N ∈ nei ⁡ J ⁡ S ∧ R ⊆ S → N ∈ nei ⁡ J ⁡ R

Proof

Step Hyp Ref Expression
1 eqid ⊢ ⋃ J = ⋃ J
2 1 neii1 ⊢ J ∈ Top ∧ N ∈ nei ⁡ J ⁡ S → N ⊆ ⋃ J
3 2 3adant3 ⊢ J ∈ Top ∧ N ∈ nei ⁡ J ⁡ S ∧ R ⊆ S → N ⊆ ⋃ J
4 neii2 ⊢ J ∈ Top ∧ N ∈ nei ⁡ J ⁡ S → ∃ g ∈ J S ⊆ g ∧ g ⊆ N
5 4 3adant3 ⊢ J ∈ Top ∧ N ∈ nei ⁡ J ⁡ S ∧ R ⊆ S → ∃ g ∈ J S ⊆ g ∧ g ⊆ N
6 sstr2 ⊢ R ⊆ S → S ⊆ g → R ⊆ g
7 6 anim1d ⊢ R ⊆ S → S ⊆ g ∧ g ⊆ N → R ⊆ g ∧ g ⊆ N
8 7 reximdv ⊢ R ⊆ S → ∃ g ∈ J S ⊆ g ∧ g ⊆ N → ∃ g ∈ J R ⊆ g ∧ g ⊆ N
9 8 3ad2ant3 ⊢ J ∈ Top ∧ N ∈ nei ⁡ J ⁡ S ∧ R ⊆ S → ∃ g ∈ J S ⊆ g ∧ g ⊆ N → ∃ g ∈ J R ⊆ g ∧ g ⊆ N
10 5 9 mpd ⊢ J ∈ Top ∧ N ∈ nei ⁡ J ⁡ S ∧ R ⊆ S → ∃ g ∈ J R ⊆ g ∧ g ⊆ N
11 simp1 ⊢ J ∈ Top ∧ N ∈ nei ⁡ J ⁡ S ∧ R ⊆ S → J ∈ Top
12 simp3 ⊢ J ∈ Top ∧ N ∈ nei ⁡ J ⁡ S ∧ R ⊆ S → R ⊆ S
13 1 neiss2 ⊢ J ∈ Top ∧ N ∈ nei ⁡ J ⁡ S → S ⊆ ⋃ J
14 13 3adant3 ⊢ J ∈ Top ∧ N ∈ nei ⁡ J ⁡ S ∧ R ⊆ S → S ⊆ ⋃ J
15 12 14 sstrd ⊢ J ∈ Top ∧ N ∈ nei ⁡ J ⁡ S ∧ R ⊆ S → R ⊆ ⋃ J
16 1 isnei ⊢ J ∈ Top ∧ R ⊆ ⋃ J → N ∈ nei ⁡ J ⁡ R ↔ N ⊆ ⋃ J ∧ ∃ g ∈ J R ⊆ g ∧ g ⊆ N
17 11 15 16 syl2anc ⊢ J ∈ Top ∧ N ∈ nei ⁡ J ⁡ S ∧ R ⊆ S → N ∈ nei ⁡ J ⁡ R ↔ N ⊆ ⋃ J ∧ ∃ g ∈ J R ⊆ g ∧ g ⊆ N
18 3 10 17 mpbir2and ⊢ J ∈ Top ∧ N ∈ nei ⁡ J ⁡ S ∧ R ⊆ S → N ∈ nei ⁡ J ⁡ R