This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑋 = ∪ 𝐽
Assertion opnssneib ( ( 𝐽 ∈ Top ∧ 𝑆 ∈ 𝐽 ∧ 𝑁 ⊆ 𝑋 ) → ( 𝑆 ⊆ 𝑁 ↔ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 neips.1 ⊢ 𝑋 = ∪ 𝐽
2 simplr ⊢ ( ( ( 𝑆 ∈ 𝐽 ∧ 𝑁 ⊆ 𝑋 ) ∧ 𝑆 ⊆ 𝑁 ) → 𝑁 ⊆ 𝑋 )
3 sseq2 ⊢ ( 𝑔 = 𝑆 → ( 𝑆 ⊆ 𝑔 ↔ 𝑆 ⊆ 𝑆 ) )
4 sseq1 ⊢ ( 𝑔 = 𝑆 → ( 𝑔 ⊆ 𝑁 ↔ 𝑆 ⊆ 𝑁 ) )
5 3 4 anbi12d ⊢ ( 𝑔 = 𝑆 → ( ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ↔ ( 𝑆 ⊆ 𝑆 ∧ 𝑆 ⊆ 𝑁 ) ) )
6 ssid ⊢ 𝑆 ⊆ 𝑆
7 6 biantrur ⊢ ( 𝑆 ⊆ 𝑁 ↔ ( 𝑆 ⊆ 𝑆 ∧ 𝑆 ⊆ 𝑁 ) )
8 5 7 bitr4di ⊢ ( 𝑔 = 𝑆 → ( ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ↔ 𝑆 ⊆ 𝑁 ) )
9 8 rspcev ⊢ ( ( 𝑆 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑁 ) → ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) )
10 9 adantlr ⊢ ( ( ( 𝑆 ∈ 𝐽 ∧ 𝑁 ⊆ 𝑋 ) ∧ 𝑆 ⊆ 𝑁 ) → ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) )
11 2 10 jca ⊢ ( ( ( 𝑆 ∈ 𝐽 ∧ 𝑁 ⊆ 𝑋 ) ∧ 𝑆 ⊆ 𝑁 ) → ( 𝑁 ⊆ 𝑋 ∧ ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) )
12 11 ex ⊢ ( ( 𝑆 ∈ 𝐽 ∧ 𝑁 ⊆ 𝑋 ) → ( 𝑆 ⊆ 𝑁 → ( 𝑁 ⊆ 𝑋 ∧ ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) ) )
13 12 3adant1 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ∈ 𝐽 ∧ 𝑁 ⊆ 𝑋 ) → ( 𝑆 ⊆ 𝑁 → ( 𝑁 ⊆ 𝑋 ∧ ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) ) )
14 1 eltopss ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ∈ 𝐽 ) → 𝑆 ⊆ 𝑋 )
15 1 isnei ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ↔ ( 𝑁 ⊆ 𝑋 ∧ ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) ) )
16 14 15 syldan ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ∈ 𝐽 ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ↔ ( 𝑁 ⊆ 𝑋 ∧ ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) ) )
17 16 3adant3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ∈ 𝐽 ∧ 𝑁 ⊆ 𝑋 ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ↔ ( 𝑁 ⊆ 𝑋 ∧ ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) ) )
18 13 17 sylibrd ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ∈ 𝐽 ∧ 𝑁 ⊆ 𝑋 ) → ( 𝑆 ⊆ 𝑁 → 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) )
19 ssnei ⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑆 ⊆ 𝑁 )
20 19 ex ⊢ ( 𝐽 ∈ Top → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) → 𝑆 ⊆ 𝑁 ) )
21 20 3ad2ant1 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ∈ 𝐽 ∧ 𝑁 ⊆ 𝑋 ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) → 𝑆 ⊆ 𝑁 ) )
22 18 21 impbid ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ∈ 𝐽 ∧ 𝑁 ⊆ 𝑋 ) → ( 𝑆 ⊆ 𝑁 ↔ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) )