Metamath Proof Explorer

Theorem opnssneib

Description: Any superset of an open set is a neighborhood of it. (Contributed by NM, 14-Feb-2007)

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

Proof

Step Hyp Ref Expression
1 neips.1 ⊢ X = ⋃ J
2 simplr ⊢ S ∈ J ∧ N ⊆ X ∧ S ⊆ N → N ⊆ X
3 sseq2 ⊢ g = S → S ⊆ g ↔ S ⊆ S
4 sseq1 ⊢ g = S → g ⊆ N ↔ S ⊆ N
5 3 4 anbi12d ⊢ g = S → S ⊆ g ∧ g ⊆ N ↔ S ⊆ S ∧ S ⊆ N
6 ssid ⊢ S ⊆ S
7 6 biantrur ⊢ S ⊆ N ↔ S ⊆ S ∧ S ⊆ N
8 5 7 bitr4di ⊢ g = S → S ⊆ g ∧ g ⊆ N ↔ S ⊆ N
9 8 rspcev ⊢ S ∈ J ∧ S ⊆ N → ∃ g ∈ J S ⊆ g ∧ g ⊆ N
10 9 adantlr ⊢ S ∈ J ∧ N ⊆ X ∧ S ⊆ N → ∃ g ∈ J S ⊆ g ∧ g ⊆ N
11 2 10 jca ⊢ S ∈ J ∧ N ⊆ X ∧ S ⊆ N → N ⊆ X ∧ ∃ g ∈ J S ⊆ g ∧ g ⊆ N
12 11 ex ⊢ S ∈ J ∧ N ⊆ X → S ⊆ N → N ⊆ X ∧ ∃ g ∈ J S ⊆ g ∧ g ⊆ N
13 12 3adant1 ⊢ J ∈ Top ∧ S ∈ J ∧ N ⊆ X → S ⊆ N → N ⊆ X ∧ ∃ g ∈ J S ⊆ g ∧ g ⊆ N
14 1 eltopss ⊢ J ∈ Top ∧ S ∈ J → S ⊆ X
15 1 isnei ⊢ J ∈ Top ∧ S ⊆ X → N ∈ nei ⁡ J ⁡ S ↔ N ⊆ X ∧ ∃ g ∈ J S ⊆ g ∧ g ⊆ N
16 14 15 syldan ⊢ J ∈ Top ∧ S ∈ J → N ∈ nei ⁡ J ⁡ S ↔ N ⊆ X ∧ ∃ g ∈ J S ⊆ g ∧ g ⊆ N
17 16 3adant3 ⊢ J ∈ Top ∧ S ∈ J ∧ N ⊆ X → N ∈ nei ⁡ J ⁡ S ↔ N ⊆ X ∧ ∃ g ∈ J S ⊆ g ∧ g ⊆ N
18 13 17 sylibrd ⊢ J ∈ Top ∧ S ∈ J ∧ N ⊆ X → S ⊆ N → N ∈ nei ⁡ J ⁡ S
19 ssnei ⊢ J ∈ Top ∧ N ∈ nei ⁡ J ⁡ S → S ⊆ N
20 19 ex ⊢ J ∈ Top → N ∈ nei ⁡ J ⁡ S → S ⊆ N
21 20 3ad2ant1 ⊢ J ∈ Top ∧ S ∈ J ∧ N ⊆ X → N ∈ nei ⁡ J ⁡ S → S ⊆ N
22 18 21 impbid ⊢ J ∈ Top ∧ S ∈ J ∧ N ⊆ X → S ⊆ N ↔ N ∈ nei ⁡ J ⁡ S