Metamath Proof Explorer

Theorem neii1

Description: A neighborhood is included in the topology's base set. (Contributed by NM, 12-Feb-2007)

Ref Expression
Hypothesis neifval.1 ⊢ X = ⋃ J
Assertion neii1 ⊢ J ∈ Top ∧ N ∈ nei ⁡ J ⁡ S → N ⊆ X

Proof

Step Hyp Ref Expression
1 neifval.1 ⊢ X = ⋃ J
2 1 neiss2 ⊢ J ∈ Top ∧ N ∈ nei ⁡ J ⁡ S → S ⊆ X
3 1 isnei ⊢ J ∈ Top ∧ S ⊆ X → N ∈ nei ⁡ J ⁡ S ↔ N ⊆ X ∧ ∃ g ∈ J S ⊆ g ∧ g ⊆ N
4 simpl ⊢ N ⊆ X ∧ ∃ g ∈ J S ⊆ g ∧ g ⊆ N → N ⊆ X
5 3 4 syl6bi ⊢ J ∈ Top ∧ S ⊆ X → N ∈ nei ⁡ J ⁡ S → N ⊆ X
6 5 impancom ⊢ J ∈ Top ∧ N ∈ nei ⁡ J ⁡ S → S ⊆ X → N ⊆ X
7 2 6 mpd ⊢ J ∈ Top ∧ N ∈ nei ⁡ J ⁡ S → N ⊆ X