Theorem ssnei2

Description: Any subset M of X containing a neighborhood N of a set S is a neighborhood of this set. Generalization to subsets of Property V_i of BourbakiTop1 p. I.3. (Contributed by FL, 2-Oct-2006)

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

Proof

Step	Hyp	Ref	Expression
1		neips.1	⊢ 𝑋 = ∪ 𝐽
2		simprr	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑁 ⊆ 𝑀 ∧ 𝑀 ⊆ 𝑋 ) ) → 𝑀 ⊆ 𝑋 )
3		neii2	⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) )
4		sstr2	⊢ ( 𝑔 ⊆ 𝑁 → ( 𝑁 ⊆ 𝑀 → 𝑔 ⊆ 𝑀 ) )
5	4	com12	⊢ ( 𝑁 ⊆ 𝑀 → ( 𝑔 ⊆ 𝑁 → 𝑔 ⊆ 𝑀 ) )
6	5	anim2d	⊢ ( 𝑁 ⊆ 𝑀 → ( ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) → ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑀 ) ) )
7	6	reximdv	⊢ ( 𝑁 ⊆ 𝑀 → ( ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) → ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑀 ) ) )
8	3 7	mpan9	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑁 ⊆ 𝑀 ) → ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑀 ) )
9	8	adantrr	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑁 ⊆ 𝑀 ∧ 𝑀 ⊆ 𝑋 ) ) → ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑀 ) )
10	1	neiss2	⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑆 ⊆ 𝑋 )
11	1	isnei	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑀 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ↔ ( 𝑀 ⊆ 𝑋 ∧ ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑀 ) ) ) )
12	10 11	syldan	⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → ( 𝑀 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ↔ ( 𝑀 ⊆ 𝑋 ∧ ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑀 ) ) ) )
13	12	adantr	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑁 ⊆ 𝑀 ∧ 𝑀 ⊆ 𝑋 ) ) → ( 𝑀 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ↔ ( 𝑀 ⊆ 𝑋 ∧ ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑀 ) ) ) )
14	2 9 13	mpbir2and	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑁 ⊆ 𝑀 ∧ 𝑀 ⊆ 𝑋 ) ) → 𝑀 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) )