Metamath Proof Explorer

Theorem neii2

Description: Property of a neighborhood. (Contributed by NM, 12-Feb-2007)

Ref Expression
Assertion neii2 ⊢ J ∈ Top ∧ N ∈ nei ⁡ J ⁡ S → ∃ g ∈ J S ⊆ g ∧ g ⊆ N

Proof

Step Hyp Ref Expression
1 eqid ⊢ ⋃ J = ⋃ J
2 1 neiss2 ⊢ J ∈ Top ∧ N ∈ nei ⁡ J ⁡ S → S ⊆ ⋃ J
3 1 isnei ⊢ J ∈ Top ∧ S ⊆ ⋃ J → N ∈ nei ⁡ J ⁡ S ↔ N ⊆ ⋃ J ∧ ∃ g ∈ J S ⊆ g ∧ g ⊆ N
4 simpr ⊢ N ⊆ ⋃ J ∧ ∃ g ∈ J S ⊆ g ∧ g ⊆ N → ∃ g ∈ J S ⊆ g ∧ g ⊆ N
5 3 4 biimtrdi ⊢ J ∈ Top ∧ S ⊆ ⋃ J → N ∈ nei ⁡ J ⁡ S → ∃ g ∈ J S ⊆ g ∧ g ⊆ N
6 5 impancom ⊢ J ∈ Top ∧ N ∈ nei ⁡ J ⁡ S → S ⊆ ⋃ J → ∃ g ∈ J S ⊆ g ∧ g ⊆ N
7 2 6 mpd ⊢ J ∈ Top ∧ N ∈ nei ⁡ J ⁡ S → ∃ g ∈ J S ⊆ g ∧ g ⊆ N