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 ⊢ X = ⋃ J
Assertion ssnei2 ⊢ J ∈ Top ∧ N ∈ nei ⁡ J ⁡ S ∧ N ⊆ M ∧ M ⊆ X → M ∈ nei ⁡ J ⁡ S

Proof

Step Hyp Ref Expression
1 neips.1 ⊢ X = ⋃ J
2 simprr ⊢ J ∈ Top ∧ N ∈ nei ⁡ J ⁡ S ∧ N ⊆ M ∧ M ⊆ X → M ⊆ X
3 neii2 ⊢ J ∈ Top ∧ N ∈ nei ⁡ J ⁡ S → ∃ g ∈ J S ⊆ g ∧ g ⊆ N
4 sstr2 ⊢ g ⊆ N → N ⊆ M → g ⊆ M
5 4 com12 ⊢ N ⊆ M → g ⊆ N → g ⊆ M
6 5 anim2d ⊢ N ⊆ M → S ⊆ g ∧ g ⊆ N → S ⊆ g ∧ g ⊆ M
7 6 reximdv ⊢ N ⊆ M → ∃ g ∈ J S ⊆ g ∧ g ⊆ N → ∃ g ∈ J S ⊆ g ∧ g ⊆ M
8 3 7 mpan9 ⊢ J ∈ Top ∧ N ∈ nei ⁡ J ⁡ S ∧ N ⊆ M → ∃ g ∈ J S ⊆ g ∧ g ⊆ M
9 8 adantrr ⊢ J ∈ Top ∧ N ∈ nei ⁡ J ⁡ S ∧ N ⊆ M ∧ M ⊆ X → ∃ g ∈ J S ⊆ g ∧ g ⊆ M
10 1 neiss2 ⊢ J ∈ Top ∧ N ∈ nei ⁡ J ⁡ S → S ⊆ X
11 1 isnei ⊢ J ∈ Top ∧ S ⊆ X → M ∈ nei ⁡ J ⁡ S ↔ M ⊆ X ∧ ∃ g ∈ J S ⊆ g ∧ g ⊆ M
12 10 11 syldan ⊢ J ∈ Top ∧ N ∈ nei ⁡ J ⁡ S → M ∈ nei ⁡ J ⁡ S ↔ M ⊆ X ∧ ∃ g ∈ J S ⊆ g ∧ g ⊆ M
13 12 adantr ⊢ J ∈ Top ∧ N ∈ nei ⁡ J ⁡ S ∧ N ⊆ M ∧ M ⊆ X → M ∈ nei ⁡ J ⁡ S ↔ M ⊆ X ∧ ∃ g ∈ J S ⊆ g ∧ g ⊆ M
14 2 9 13 mpbir2and ⊢ J ∈ Top ∧ N ∈ nei ⁡ J ⁡ S ∧ N ⊆ M ∧ M ⊆ X → M ∈ nei ⁡ J ⁡ S