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

Metamath Proof Explorer

Theorem opnneissb

Description: An open set is a neighborhood of any of its subsets. (Contributed by FL, 2-Oct-2006)

Ref Expression
Hypothesis neips.1 ⊢ 𝑋 = ∪ 𝐽
Assertion opnneissb ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑆 ⊆ 𝑁 ↔ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 neips.1 ⊢ 𝑋 = ∪ 𝐽
2 1 eltopss ⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ 𝐽 ) → 𝑁 ⊆ 𝑋 )
3 2 adantr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ 𝐽 ) ∧ ( 𝑆 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑁 ) ) → 𝑁 ⊆ 𝑋 )
4 ssid ⊢ 𝑁 ⊆ 𝑁
5 sseq2 ⊢ ( 𝑔 = 𝑁 → ( 𝑆 ⊆ 𝑔 ↔ 𝑆 ⊆ 𝑁 ) )
6 sseq1 ⊢ ( 𝑔 = 𝑁 → ( 𝑔 ⊆ 𝑁 ↔ 𝑁 ⊆ 𝑁 ) )
7 5 6 anbi12d ⊢ ( 𝑔 = 𝑁 → ( ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ↔ ( 𝑆 ⊆ 𝑁 ∧ 𝑁 ⊆ 𝑁 ) ) )
8 7 rspcev ⊢ ( ( 𝑁 ∈ 𝐽 ∧ ( 𝑆 ⊆ 𝑁 ∧ 𝑁 ⊆ 𝑁 ) ) → ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) )
9 4 8 mpanr2 ⊢ ( ( 𝑁 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑁 ) → ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) )
10 9 ad2ant2l ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ 𝐽 ) ∧ ( 𝑆 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑁 ) ) → ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) )
11 1 isnei ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ↔ ( 𝑁 ⊆ 𝑋 ∧ ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) ) )
12 11 ad2ant2r ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ 𝐽 ) ∧ ( 𝑆 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑁 ) ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ↔ ( 𝑁 ⊆ 𝑋 ∧ ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) ) )
13 3 10 12 mpbir2and ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ 𝐽 ) ∧ ( 𝑆 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑁 ) ) → 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) )
14 13 exp43 ⊢ ( 𝐽 ∈ Top → ( 𝑁 ∈ 𝐽 → ( 𝑆 ⊆ 𝑋 → ( 𝑆 ⊆ 𝑁 → 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ) ) )
15 14 3imp ⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑆 ⊆ 𝑁 → 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) )
16 ssnei ⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑆 ⊆ 𝑁 )
17 16 ex ⊢ ( 𝐽 ∈ Top → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) → 𝑆 ⊆ 𝑁 ) )
18 17 3ad2ant1 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) → 𝑆 ⊆ 𝑁 ) )
19 15 18 impbid ⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑆 ⊆ 𝑁 ↔ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) )