Metamath Proof Explorer

Theorem neissex

Description: For any neighborhood N of S , there is a neighborhood x of S such that N is a neighborhood of all subsets of x . Generalization to subsets of Property V_iv of BourbakiTop1 p. I.3. (Contributed by FL, 2-Oct-2006)

Ref Expression
Assertion neissex ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → ∃ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∀ 𝑦 ( 𝑦 ⊆ 𝑥 → 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 neii2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → ∃ 𝑥 ∈ 𝐽 ( 𝑆 ⊆ 𝑥 ∧ 𝑥 ⊆ 𝑁 ) )
2 opnneiss ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑥 ) → 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) )
3 2 3expb ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑥 ) ) → 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) )
4 3 adantrrr ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑆 ⊆ 𝑥 ∧ 𝑥 ⊆ 𝑁 ) ) ) → 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) )
5 4 adantlr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑆 ⊆ 𝑥 ∧ 𝑥 ⊆ 𝑁 ) ) ) → 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) )
6 simplll ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝑁 ) ) ∧ 𝑦 ⊆ 𝑥 ) → 𝐽 ∈ Top )
7 simpll ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝐽 ) → 𝐽 ∈ Top )
8 simpr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝐽 ) → 𝑥 ∈ 𝐽 )
9 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
10 9 neii1 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑁 ⊆ ∪ 𝐽 )
11 10 adantr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝐽 ) → 𝑁 ⊆ ∪ 𝐽 )
12 9 opnssneib ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ∧ 𝑁 ⊆ ∪ 𝐽 ) → ( 𝑥 ⊆ 𝑁 ↔ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑥 ) ) )
13 7 8 11 12 syl3anc ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝐽 ) → ( 𝑥 ⊆ 𝑁 ↔ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑥 ) ) )
14 13 biimpa ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑥 ⊆ 𝑁 ) → 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑥 ) )
15 14 anasss ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝑁 ) ) → 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑥 ) )
16 15 adantr ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝑁 ) ) ∧ 𝑦 ⊆ 𝑥 ) → 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑥 ) )
17 simpr ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝑁 ) ) ∧ 𝑦 ⊆ 𝑥 ) → 𝑦 ⊆ 𝑥 )
18 neiss ⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑥 ) ∧ 𝑦 ⊆ 𝑥 ) → 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑦 ) )
19 6 16 17 18 syl3anc ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝑁 ) ) ∧ 𝑦 ⊆ 𝑥 ) → 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑦 ) )
20 19 ex ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝑁 ) ) → ( 𝑦 ⊆ 𝑥 → 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑦 ) ) )
21 20 adantrrl ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑆 ⊆ 𝑥 ∧ 𝑥 ⊆ 𝑁 ) ) ) → ( 𝑦 ⊆ 𝑥 → 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑦 ) ) )
22 21 alrimiv ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑆 ⊆ 𝑥 ∧ 𝑥 ⊆ 𝑁 ) ) ) → ∀ 𝑦 ( 𝑦 ⊆ 𝑥 → 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑦 ) ) )
23 1 5 22 reximssdv ⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → ∃ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∀ 𝑦 ( 𝑦 ⊆ 𝑥 → 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑦 ) ) )