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 ‘ 𝐽 ) ‘ 𝑆 ) ) )