Theorem neiss

Description: Any neighborhood of a set S is also a neighborhood of any subset R C_ S . Similar to Proposition 1 of BourbakiTop1 p. I.2. (Contributed by FL, 25-Sep-2006)

	Ref	Expression
Assertion	neiss	⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑅 ⊆ 𝑆 ) → 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
2	1	neii1	⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑁 ⊆ ∪ 𝐽 )
3	2	3adant3	⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑅 ⊆ 𝑆 ) → 𝑁 ⊆ ∪ 𝐽 )
4		neii2	⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) )
5	4	3adant3	⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑅 ⊆ 𝑆 ) → ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) )
6		sstr2	⊢ ( 𝑅 ⊆ 𝑆 → ( 𝑆 ⊆ 𝑔 → 𝑅 ⊆ 𝑔 ) )
7	6	anim1d	⊢ ( 𝑅 ⊆ 𝑆 → ( ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) → ( 𝑅 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) )
8	7	reximdv	⊢ ( 𝑅 ⊆ 𝑆 → ( ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) → ∃ 𝑔 ∈ 𝐽 ( 𝑅 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) )
9	8	3ad2ant3	⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑅 ⊆ 𝑆 ) → ( ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) → ∃ 𝑔 ∈ 𝐽 ( 𝑅 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) )
10	5 9	mpd	⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑅 ⊆ 𝑆 ) → ∃ 𝑔 ∈ 𝐽 ( 𝑅 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) )
11		simp1	⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑅 ⊆ 𝑆 ) → 𝐽 ∈ Top )
12		simp3	⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑅 ⊆ 𝑆 ) → 𝑅 ⊆ 𝑆 )
13	1	neiss2	⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑆 ⊆ ∪ 𝐽 )
14	13	3adant3	⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑅 ⊆ 𝑆 ) → 𝑆 ⊆ ∪ 𝐽 )
15	12 14	sstrd	⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑅 ⊆ 𝑆 ) → 𝑅 ⊆ ∪ 𝐽 )
16	1	isnei	⊢ ( ( 𝐽 ∈ Top ∧ 𝑅 ⊆ ∪ 𝐽 ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑅 ) ↔ ( 𝑁 ⊆ ∪ 𝐽 ∧ ∃ 𝑔 ∈ 𝐽 ( 𝑅 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) ) )
17	11 15 16	syl2anc	⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑅 ⊆ 𝑆 ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑅 ) ↔ ( 𝑁 ⊆ ∪ 𝐽 ∧ ∃ 𝑔 ∈ 𝐽 ( 𝑅 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) ) )
18	3 10 17	mpbir2and	⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑅 ⊆ 𝑆 ) → 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑅 ) )