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