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∈JS⊆g∧g⊆N
10 9 adantlr ⊢S∈J∧N⊆X∧S⊆N→∃g∈JS⊆g∧g⊆N
11 2 10 jca ⊢S∈J∧N⊆X∧S⊆N→N⊆X∧∃g∈JS⊆g∧g⊆N
12 11 ex ⊢S∈J∧N⊆X→S⊆N→N⊆X∧∃g∈JS⊆g∧g⊆N
13 12 3adant1 ⊢J∈Top∧S∈J∧N⊆X→S⊆N→N⊆X∧∃g∈JS⊆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∈JS⊆g∧g⊆N
16 14 15 syldan ⊢J∈Top∧S∈J→N∈nei⁡J⁡S↔N⊆X∧∃g∈JS⊆g∧g⊆N
17 16 3adant3 ⊢J∈Top∧S∈J∧N⊆X→N∈nei⁡J⁡S↔N⊆X∧∃g∈JS⊆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